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 form). (Contributed by NM, 26-May-1993.) Avoid ax-11 2162. (Revised by Wolf Lammen, 6-May-2023.) |
Ref | Expression |
---|---|
abbi2i.1 | ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Ref | Expression |
---|---|
abbi2i | ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbi2i.1 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑)) |
3 | 2 | abbi2dv 2869 | . 2 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑}) |
4 | 3 | mptru 1549 | 1 ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1542 ⊤wtru 1543 ∈ wcel 2114 {cab 2716 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 |
This theorem is referenced by: abid1 2873 cbvralcsf 3832 cbvreucsf 3834 cbvrabcsf 3835 dfsymdif4 4139 dfsymdif2 4141 dfpr2 4535 dftp2 4580 0iin 4949 pwpwab 4988 epse 5508 pwvabrel 5574 fv3 6692 fo1st 7734 fo2nd 7735 xp2 7751 tfrlem3 8043 ixpconstg 8516 ixp0x 8536 ruv 9139 dfom4 9185 cardnum 9594 alephiso 9598 nnzrab 12091 nn0zrab 12092 qnnen 15658 h2hcau 28914 dfch2 29342 hhcno 29839 hhcnf 29840 pjhmopidm 30118 bdayfo 33521 madeval2 33678 fobigcup 33840 dfsingles2 33861 dfrecs2 33890 dfrdg4 33891 dfint3 33892 bj-snglinv 34785 ecres 36036 dfdm6 36060 ruvALT 39759 compeq 41596 dfnrm2 45747 dfnrm3 45748 |
Copyright terms: Public domain | W3C validator |