![]() |
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 3621 | . 2 ⊢ ((𝜓 → 𝐴 ∈ V) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1538 ∈ wcel 2111 {cab 2776 Vcvv 3441 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-v 3443 |
This theorem is referenced by: fvelrnb 6701 elrnmpo 7266 ovelrn 7304 isfi 8516 isnum2 9358 pm54.43lem 9413 isfin3 9707 isfin5 9710 isfin6 9711 genpelv 10411 iswrd 13859 4sqlem2 16275 vdwapval 16299 isghm 18350 issrng 19614 lspsnel 19768 lspprel 19859 iscss 20372 ellspd 20491 istps 21539 islp 21745 is2ndc 22051 elpt 22177 itg2l 24333 elply 24792 isismt 26328 bj-ififc 34028 isline 37035 ispointN 37038 ispsubsp 37041 ispsubclN 37233 islaut 37379 ispautN 37395 istendo 38056 rngunsnply 40117 |
Copyright terms: Public domain | W3C validator |