![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqabi | Structured version Visualization version GIF version |
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2146. (Revised by Wolf Lammen, 6-May-2023.) |
Ref | Expression |
---|---|
eqabi.1 | ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Ref | Expression |
---|---|
eqabi | ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqabi.1 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑)) |
3 | 2 | eqabdv 2859 | . 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑}) |
4 | 3 | mptru 1540 | 1 ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 ⊤wtru 1534 ∈ wcel 2098 {cab 2702 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 |
This theorem is referenced by: abid1 2862 cbvralcsf 3934 cbvreucsf 3936 cbvrabcsf 3937 dfsymdif4 4247 dfsymdif2 4249 dfpr2 4650 dftp2 4695 iunid 5064 0iin 5068 pwpwab 5107 epse 5661 pwvabrel 5729 fv3 6914 fo1st 8014 fo2nd 8015 xp2 8031 tfrlem3 8399 ixpconstg 8925 ixp0x 8945 ruv 9627 dfom4 9674 cardnum 10119 alephiso 10123 nnzrab 12623 nn0zrab 12624 qnnen 16193 bdayfo 27656 madeval2 27826 h2hcau 30861 dfch2 31289 hhcno 31786 hhcnf 31787 pjhmopidm 32065 fobigcup 35627 dfsingles2 35648 dfrecs2 35677 dfrdg4 35678 dfint3 35679 bj-snglinv 36582 ecres 37880 dfdm6 37903 ruvALT 42228 rp-abid 42949 dfuniv2 43881 compeq 44019 dfnrm2 48136 dfnrm3 48137 |
Copyright terms: Public domain | W3C validator |