Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elab3 | Structured version Visualization version GIF version |
Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.) |
Ref | Expression |
---|---|
elab3.1 | ⊢ (𝜓 → 𝐴 ∈ V) |
elab3.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elab3 | ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab3.1 | . 2 ⊢ (𝜓 → 𝐴 ∈ V) | |
2 | elab3.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | elab3g 3326 | . 2 ⊢ ((𝜓 → 𝐴 ∈ V) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∈ wcel 1977 {cab 2596 Vcvv 3173 |
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-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 |
This theorem is referenced by: fvelrnb 6153 elrnmpt2 6671 ovelrn 6708 isfi 7865 isnum2 8654 pm54.43lem 8708 isfin3 9001 isfin5 9004 isfin6 9005 genpelv 9701 iswrd 13162 4sqlem2 15491 vdwapval 15515 isghm 17483 issrng 18673 lspsnel 18824 lspprel 18915 iscss 19846 ellspd 19960 istps 20551 islp 20754 is2ndc 21059 elpt 21185 itg2l 23302 elply 23755 isismt 25229 isline 34043 ispointN 34046 ispsubsp 34049 ispsubclN 34241 islaut 34387 ispautN 34403 istendo 35066 rngunsnply 36762 |
Copyright terms: Public domain | W3C validator |