![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > abbi2i | Structured version Visualization version GIF version |
Description: Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
abbi2i.1 | ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Ref | Expression |
---|---|
abbi2i | ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abeq2 2761 | . 2 ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | |
2 | abbi2i.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | |
3 | 1, 2 | mpgbir 1766 | 1 ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1523 ∈ wcel 2030 {cab 2637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 |
This theorem is referenced by: abid1 2773 cbvralcsf 3598 cbvreucsf 3600 cbvrabcsf 3601 dfsymdif2 3884 symdif2 3885 dfnul2 3950 dfpr2 4228 dftp2 4263 0iin 4610 pwpwab 4646 epse 5126 fv3 6244 fo1st 7230 fo2nd 7231 xp2 7247 tfrlem3 7519 mapsn 7941 ixpconstg 7959 ixp0x 7978 dfom4 8584 cardnum 8955 alephiso 8959 nnzrab 11443 nn0zrab 11444 qnnen 14986 h2hcau 27964 dfch2 28394 hhcno 28891 hhcnf 28892 pjhmopidm 29170 bdayfo 31953 madeval2 32061 fobigcup 32132 dfsingles2 32153 dfrecs2 32182 dfrdg4 32183 dfint3 32184 bj-snglinv 33085 ecres 34184 dfdm6 34212 compeq 38959 |
Copyright terms: Public domain | W3C validator |