![]() |
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 2868 | . 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑}) |
4 | 3 | mptru 1549 | 1 ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1542 ⊤wtru 1543 ∈ wcel 2107 {cab 2710 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 |
This theorem is referenced by: abid1 2871 cbvralcsf 3936 cbvreucsf 3938 cbvrabcsf 3939 dfsymdif4 4246 dfsymdif2 4248 dfpr2 4643 dftp2 4689 iunid 5059 0iin 5063 pwpwab 5102 epse 5655 pwvabrel 5722 fv3 6899 fo1st 7982 fo2nd 7983 xp2 7999 tfrlem3 8365 ixpconstg 8888 ixp0x 8908 ruv 9584 dfom4 9631 cardnum 10076 alephiso 10080 nnzrab 12577 nn0zrab 12578 qnnen 16143 bdayfo 27147 madeval2 27315 h2hcau 30197 dfch2 30625 hhcno 31122 hhcnf 31123 pjhmopidm 31401 fobigcup 34803 dfsingles2 34824 dfrecs2 34853 dfrdg4 34854 dfint3 34855 bj-snglinv 35758 ecres 37052 dfdm6 37076 ruvALT 40934 rp-abid 41999 dfuniv2 42932 compeq 43070 dfnrm2 47404 dfnrm3 47405 |
Copyright terms: Public domain | W3C validator |