![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elabg | Structured version Visualization version GIF version |
Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2372. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2138, ax-11 2155, ax-12 2172. (Revised by SN, 5-Oct-2024.) |
Ref | Expression |
---|---|
elabg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elabg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab6g 3658 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) | |
2 | elabg.1 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | pm5.74i 271 | . . . . 5 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓)) |
4 | 3 | albii 1822 | . . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
5 | 19.23v 1946 | . . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) | |
6 | 4, 5 | bitri 275 | . . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
7 | elisset 2816 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
8 | pm5.5 362 | . . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓)) | |
9 | 7, 8 | syl 17 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓)) |
10 | 6, 9 | bitrid 283 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)) |
11 | 1, 10 | bitrd 279 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 = wceq 1542 ∃wex 1782 ∈ wcel 2107 {cab 2710 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 |
This theorem is referenced by: elab 3667 elab2g 3669 elabd 3670 elab3g 3674 sbcieg 3816 intmin3 4979 finds 7884 elfi 9404 inficl 9416 dffi3 9422 scott0 9877 elgch 10613 nqpr 11005 hashf1lem1 14411 hashf1lem1OLD 14412 cshword 14737 trclublem 14938 cotrtrclfv 14955 dfiso2 17715 efgcpbllemb 19616 frgpuplem 19633 lspsn 20601 mpfind 21652 pf1ind 21856 eltg 22442 eltg2 22443 islocfin 23003 fbssfi 23323 nosupres 27190 nosupbnd1lem3 27193 nosupbnd1lem5 27195 noinffv 27204 noinfres 27205 noinfbnd1lem3 27208 noinfbnd1lem5 27210 isewlk 28839 elabreximd 31725 abfmpunirn 31855 fmlafvel 34314 isfmlasuc 34317 poimirlem3 36429 poimirlem25 36451 islshpkrN 37928 sticksstones8 40907 sticksstones9 40908 sticksstones11 40910 sticksstones17 40917 sticksstones18 40918 sn-iotalem 40986 setindtrs 41697 frege55lem1c 42600 nzss 43009 elabrexg 43661 afvelrnb 45806 afvelrnb0 45807 dfatco 45899 elsetpreimafvb 45987 setis 47645 |
Copyright terms: Public domain | W3C validator |