![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elab2gw | Structured version Visualization version GIF version |
Description: Membership in a class abstraction, using implicit substitution and an intermediate setvar 𝑦 to avoid ax-10 2143, ax-11 2159, ax-12 2176. It also avoids a disjoint variable condition on 𝑥 and 𝐴. (Contributed by SN, 16-May-2024.) |
Ref | Expression |
---|---|
elabgw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
elabgw.2 | ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) |
elab2gw.3 | ⊢ 𝐵 = {𝑥 ∣ 𝜑} |
Ref | Expression |
---|---|
elab2gw | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab2gw.3 | . . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑} | |
2 | 1 | eleq2i 2842 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
3 | elabgw.1 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | elabgw.2 | . . 3 ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) | |
5 | 3, 4 | elabgw 3583 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒)) |
6 | 2, 5 | syl5bb 286 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1539 ∈ wcel 2112 {cab 2736 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2730 |
This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1783 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 |
This theorem is referenced by: rru 3690 eldif 3864 elin 3870 elun 4050 elpwg 4490 elsng 4529 elprg 4536 dfopif 4750 eluni 4794 elint 4837 elintg 4839 eliun 4880 eliin 4881 elopab 5377 elxpi 5539 elrn2g 5723 eldmg 5731 elong 6170 isfin2 9739 iswun 10149 elnpi 10433 issal 43307 |
Copyright terms: Public domain | W3C validator |