![]() |
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 2763 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑)) |
4 | 3 | trud 1533 | 1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1523 ⊤wtru 1524 ∈ 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-12 2087 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-tru 1526 df-ex 1745 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 |
This theorem is referenced by: abeq1i 2765 rabid 3145 vex 3234 csbco 3576 csbnestgf 4029 ssrel 5241 relopabi 5278 cnv0 5570 funcnv3 5997 opabiota 6300 zfrep6 7176 wfrlem2 7460 wfrlem3 7461 wfrlem4 7463 wfrdmcl 7468 tfrlem4 7520 tfrlem8 7525 tfrlem9 7526 ixpn0 7982 mapsnen 8076 sbthlem1 8111 dffi3 8378 1idpr 9889 ltexprlem1 9896 ltexprlem2 9897 ltexprlem3 9898 ltexprlem4 9899 ltexprlem6 9901 ltexprlem7 9902 reclem2pr 9908 reclem3pr 9909 reclem4pr 9910 supsrlem 9970 dissnref 21379 dissnlocfin 21380 txbas 21418 xkoccn 21470 xkoptsub 21505 xkoco1cn 21508 xkoco2cn 21509 xkoinjcn 21538 mbfi1fseqlem4 23530 avril1 27449 rnmpt2ss 29601 bnj1436 31036 bnj916 31129 bnj983 31147 bnj1083 31172 bnj1245 31208 bnj1311 31218 bnj1371 31223 bnj1398 31228 setinds 31807 frrlem2 31906 frrlem3 31907 frrlem4 31908 frrlem5e 31913 frrlem11 31917 bj-ififc 32691 bj-elsngl 33081 bj-projun 33107 bj-projval 33109 f1omptsnlem 33313 icoreresf 33330 finxp0 33358 finxp1o 33359 finxpsuclem 33364 sdclem1 33669 csbcom2fi 34064 csbgfi 34065 |
Copyright terms: Public domain | W3C validator |