![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elab2 | Structured version Visualization version GIF version |
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elab2.1 | ⊢ 𝐴 ∈ V |
elab2.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
elab2.3 | ⊢ 𝐵 = {𝑥 ∣ 𝜑} |
Ref | Expression |
---|---|
elab2 | ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab2.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | elab2.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | elab2.3 | . . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑} | |
4 | 2, 3 | elab2g 3494 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1632 ∈ wcel 2140 {cab 2747 Vcvv 3341 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2048 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-v 3343 |
This theorem is referenced by: elpw 4309 elint 4634 opabid 5133 elrn2 5521 elimasn 5649 oprabid 6842 wfrlem3a 7588 tfrlem3a 7644 cardprclem 9016 iunfictbso 9148 aceq3lem 9154 dfac5lem4 9160 kmlem9 9193 domtriomlem 9477 ltexprlem3 10073 ltexprlem4 10074 reclem2pr 10083 reclem3pr 10084 supsrlem 10145 supaddc 11203 supadd 11204 supmul1 11205 supmullem1 11206 supmullem2 11207 supmul 11208 sqrlem6 14208 infcvgaux2i 14810 mertenslem1 14836 mertenslem2 14837 4sqlem12 15883 conjnmzb 17917 sylow3lem2 18264 mdetunilem9 20649 txuni2 21591 xkoopn 21615 met2ndci 22549 2sqlem8 25372 2sqlem11 25375 eulerpartlemt 30764 eulerpartlemr 30767 eulerpartlemn 30774 subfacp1lem3 31493 subfacp1lem5 31495 soseq 32082 finxpsuclem 33564 heiborlem1 33942 heiborlem6 33947 heiborlem8 33949 cllem0 38392 |
Copyright terms: Public domain | W3C validator |