![]() |
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 2155. (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 2873 | . 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑}) |
4 | 3 | mptru 1544 | 1 ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 = wceq 1537 ⊤wtru 1538 ∈ wcel 2106 {cab 2712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 |
This theorem is referenced by: abid1 2876 cbvralcsf 3953 cbvreucsf 3955 cbvrabcsf 3956 dfsymdif4 4265 dfsymdif2 4267 dfpr2 4651 dftp2 4696 iunid 5065 0iin 5069 pwpwab 5108 epse 5671 pwvabrel 5740 fv3 6925 fo1st 8033 fo2nd 8034 xp2 8050 tfrlem3 8417 ixpconstg 8945 ixp0x 8965 ruv 9640 dfom4 9687 cardnum 10132 alephiso 10136 nnzrab 12643 nn0zrab 12644 qnnen 16246 bdayfo 27737 madeval2 27907 h2hcau 31008 dfch2 31436 hhcno 31933 hhcnf 31934 pjhmopidm 32212 fobigcup 35882 dfsingles2 35903 dfrecs2 35932 dfrdg4 35933 dfint3 35934 bj-snglinv 36955 ecres 38260 dfdm6 38283 ruvALT 42656 rp-abid 43368 dfuniv2 44298 compeq 44436 dfnrm2 48728 dfnrm3 48729 |
Copyright terms: Public domain | W3C validator |