![]() |
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 3578 | . 2 ⊢ ((𝜓 → 𝐴 ∈ V) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1658 ∈ wcel 2166 {cab 2811 Vcvv 3414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 |
This theorem is referenced by: fvelrnb 6490 elrnmpt2 7033 ovelrn 7070 isfi 8246 isnum2 9084 pm54.43lem 9138 isfin3 9433 isfin5 9436 isfin6 9437 genpelv 10137 iswrd 13576 4sqlem2 16024 vdwapval 16048 isghm 18011 issrng 19206 lspsnel 19362 lspprel 19453 iscss 20390 ellspd 20508 istps 21109 islp 21315 is2ndc 21620 elpt 21746 itg2l 23895 elply 24350 isismt 25846 isline 35814 ispointN 35817 ispsubsp 35820 ispsubclN 36012 islaut 36158 ispautN 36174 istendo 36835 rngunsnply 38586 |
Copyright terms: Public domain | W3C validator |