| 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 3685 | . 2 ⊢ ((𝜓 → 𝐴 ∈ 𝑉) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
| 4 | 1, 3 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 {cab 2714 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 |
| This theorem is referenced by: fvelrnb 6969 elrnmpo 7569 ovelrn 7609 isfi 9016 isnum2 9985 pm54.43lem 10040 isfin3 10336 isfin5 10339 isfin6 10340 genpelv 11040 iswrd 14554 4sqlem2 16987 vdwapval 17011 isghm 19233 isghmOLD 19234 issrng 20845 ellspsn 21001 lspprel 21093 iscss 21701 ellspd 21822 istps 22940 islp 23148 is2ndc 23454 elpt 23580 itg2l 25764 elply 26234 isismt 28542 bj-ififc 36583 isline 39741 ispointN 39744 ispsubsp 39747 ispsubclN 39939 islaut 40085 ispautN 40101 istendo 40762 sn-isghm 42683 rngunsnply 43181 |
| Copyright terms: Public domain | W3C validator |