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 2719 | . 2 ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | |
2 | abbi2i.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | |
3 | 1, 2 | mpgbir 1717 | 1 ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ∈ wcel 1977 {cab 2596 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 |
This theorem is referenced by: abid1 2731 cbvralcsf 3531 cbvreucsf 3533 cbvrabcsf 3534 dfsymdif2 3813 symdif2 3814 dfnul2 3876 dfpr2 4143 dftp2 4178 0iin 4514 epse 5021 fv3 6116 fo1st 7079 fo2nd 7080 xp2 7094 tfrlem3 7361 mapsn 7785 ixpconstg 7803 ixp0x 7822 dfom4 8429 cardnum 8800 alephiso 8804 nnzrab 11282 nn0zrab 11283 qnnen 14781 h2hcau 27220 dfch2 27650 hhcno 28147 hhcnf 28148 pjhmopidm 28426 bdayfo 31074 fobigcup 31177 dfsingles2 31198 dfrecs2 31227 dfrdg4 31228 dfint3 31229 bj-snglinv 32153 compeq 37664 |
Copyright terms: Public domain | W3C validator |