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 3353 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1483 ∈ wcel 1990 {cab 2608 Vcvv 3200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 |
This theorem is referenced by: elpw 4164 elint 4481 opabid 4982 elrn2 5365 elimasn 5490 oprabid 6677 wfrlem3a 7417 tfrlem3a 7473 cardprclem 8805 iunfictbso 8937 aceq3lem 8943 dfac5lem4 8949 kmlem9 8980 domtriomlem 9264 ltexprlem3 9860 ltexprlem4 9861 reclem2pr 9870 reclem3pr 9871 supsrlem 9932 supaddc 10990 supadd 10991 supmul1 10992 supmullem1 10993 supmullem2 10994 supmul 10995 sqrlem6 13988 infcvgaux2i 14590 mertenslem1 14616 mertenslem2 14617 4sqlem12 15660 conjnmzb 17695 sylow3lem2 18043 mdetunilem9 20426 txuni2 21368 xkoopn 21392 met2ndci 22327 2sqlem8 25151 2sqlem11 25154 eulerpartlemt 30433 eulerpartlemr 30436 eulerpartlemn 30443 subfacp1lem3 31164 subfacp1lem5 31166 soseq 31751 finxpsuclem 33234 heiborlem1 33610 heiborlem6 33615 heiborlem8 33617 cllem0 37871 |
Copyright terms: Public domain | W3C validator |