![]() |
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.) (Revised by AV, 16-Aug-2024.) |
Ref | Expression |
---|---|
elab3.1 | ⊢ (𝜓 → 𝐴 ∈ 𝑉) |
elab3.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elab3 | ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab3.1 | . 2 ⊢ (𝜓 → 𝐴 ∈ 𝑉) | |
2 | elab3.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | elab3g 3672 | . 2 ⊢ ((𝜓 → 𝐴 ∈ 𝑉) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 {cab 2704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 |
This theorem is referenced by: fvelrnb 6953 elrnmpo 7551 ovelrn 7591 isfi 8988 isnum2 9960 pm54.43lem 10015 isfin3 10311 isfin5 10314 isfin6 10315 genpelv 11015 iswrd 14490 4sqlem2 16909 vdwapval 16933 isghm 19161 issrng 20719 lspsnel 20876 lspprel 20968 iscss 21602 ellspd 21723 istps 22823 islp 23031 is2ndc 23337 elpt 23463 itg2l 25646 elply 26116 isismt 28325 bj-ififc 35994 isline 39149 ispointN 39152 ispsubsp 39155 ispsubclN 39347 islaut 39493 ispautN 39509 istendo 40170 rngunsnply 42519 |
Copyright terms: Public domain | W3C validator |