Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > abeq2i | Structured version Visualization version GIF version |
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.) |
Ref | Expression |
---|---|
abeq2i.1 | ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Ref | Expression |
---|---|
abeq2i | ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abeq2i.1 | . . . 4 ⊢ 𝐴 = {𝑥 ∣ 𝜑} | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑}) |
3 | 2 | abeq2d 2871 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑)) |
4 | 3 | mptru 1550 | 1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ⊤wtru 1544 ∈ wcel 2110 {cab 2714 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-12 2175 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 |
This theorem is referenced by: abeq1i 2873 rabid 3287 csbcow 3823 csbco 3824 csbgfi 3829 csbnestgfw 4331 csbnestgf 4336 ssrel 5651 relopabi 5689 cnv0 6001 funcnv3 6447 opabiota 6791 zfrep6 7725 frrlem2 8025 frrlem3 8026 frrlem4 8027 frrlem8 8031 wfrlem2 8052 wfrlem3 8053 wfrlem4 8055 wfrdmcl 8060 tfrlem4 8112 tfrlem8 8117 tfrlem9 8118 ixpn0 8608 sbthlem1 8753 dffi3 9044 1idpr 10640 ltexprlem1 10647 ltexprlem2 10648 ltexprlem3 10649 ltexprlem4 10650 ltexprlem6 10652 ltexprlem7 10653 reclem2pr 10659 reclem3pr 10660 reclem4pr 10661 supsrlem 10722 dissnref 22422 dissnlocfin 22423 txbas 22461 xkoccn 22513 xkoptsub 22548 xkoco1cn 22551 xkoco2cn 22552 xkoinjcn 22581 mbfi1fseqlem4 24613 avril1 28543 rnmposs 30728 bnj1436 32529 bnj916 32623 bnj983 32641 bnj1083 32668 bnj1245 32704 bnj1311 32714 bnj1371 32719 bnj1398 32724 setinds 33470 bj-elsngl 34892 bj-projun 34918 bj-projval 34920 f1omptsnlem 35241 icoreresf 35257 finxp0 35296 finxp1o 35297 finxpsuclem 35302 sdclem1 35636 csbcom2fi 36021 rr-grothshortbi 41592 |
Copyright terms: Public domain | W3C validator |