![]() |
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 3674 | . 2 ⊢ ((𝜓 → 𝐴 ∈ 𝑉) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∈ wcel 2098 {cab 2704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 |
This theorem is referenced by: fvelrnb 6962 elrnmpo 7561 ovelrn 7601 isfi 9001 isnum2 9974 pm54.43lem 10029 isfin3 10325 isfin5 10328 isfin6 10329 genpelv 11029 iswrd 14504 4sqlem2 16923 vdwapval 16947 isghm 19175 issrng 20735 lspsnel 20892 lspprel 20984 iscss 21620 ellspd 21741 istps 22854 islp 23062 is2ndc 23368 elpt 23494 itg2l 25677 elply 26147 isismt 28356 bj-ififc 36063 isline 39216 ispointN 39219 ispsubsp 39222 ispsubclN 39414 islaut 39560 ispautN 39576 istendo 40237 rngunsnply 42600 |
Copyright terms: Public domain | W3C validator |