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 rule). (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 2721 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑)) |
4 | 3 | trud 1484 | 1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ⊤wtru 1476 ∈ 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-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-tru 1478 df-ex 1696 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 |
This theorem is referenced by: abeq1i 2723 rabid 3095 vex 3176 csbco 3509 csbnestgf 3948 ssrel 5130 relopabi 5167 cnv0 5454 funcnv3 5873 opabiota 6171 zfrep6 7027 wfrlem2 7302 wfrlem3 7303 wfrlem4 7305 wfrdmcl 7310 tfrlem4 7362 tfrlem8 7367 tfrlem9 7368 ixpn0 7826 mapsnen 7920 sbthlem1 7955 dffi3 8220 1idpr 9730 ltexprlem1 9737 ltexprlem2 9738 ltexprlem3 9739 ltexprlem4 9740 ltexprlem6 9742 ltexprlem7 9743 reclem2pr 9749 reclem3pr 9750 reclem4pr 9751 supsrlem 9811 dissnref 21141 dissnlocfin 21142 txbas 21180 xkoccn 21232 xkoptsub 21267 xkoco1cn 21270 xkoco2cn 21271 xkoinjcn 21300 mbfi1fseqlem4 23291 avril1 26711 rnmpt2ss 28856 bnj1436 30164 bnj916 30257 bnj983 30275 bnj1083 30300 bnj1245 30336 bnj1311 30346 bnj1371 30351 bnj1398 30356 setinds 30927 frrlem2 31025 frrlem3 31026 frrlem4 31027 frrlem5e 31032 frrlem11 31036 bj-ififc 31736 bj-elsngl 32149 bj-projun 32175 bj-projval 32177 f1omptsnlem 32359 icoreresf 32376 finxp0 32404 finxp1o 32405 finxpsuclem 32410 sdclem1 32709 csbcom2fi 33104 csbgfi 33105 |
Copyright terms: Public domain | W3C validator |