![]() |
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 2366. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2130, ax-11 2147, ax-12 2164. (Revised by SN, 5-Oct-2024.) |
Ref | Expression |
---|---|
elabg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elabg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab6g 3655 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))) | |
2 | elabg.1 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | pm5.74i 271 | . . . . 5 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓)) |
4 | 3 | albii 1814 | . . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓)) |
5 | 19.23v 1938 | . . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) | |
6 | 4, 5 | bitri 275 | . . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)) |
7 | elisset 2810 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
8 | pm5.5 361 | . . . 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 1532 = wceq 1534 ∃wex 1774 ∈ 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: elab 3665 elab2g 3667 elabd 3668 elab3g 3672 sbcieg 3814 intmin3 4974 elabrexg 7247 finds 7898 elfi 9428 inficl 9440 dffi3 9446 scott0 9901 elgch 10637 nqpr 11029 hashf1lem1 14439 hashf1lem1OLD 14440 cshword 14765 trclublem 14966 cotrtrclfv 14983 dfiso2 17746 efgcpbllemb 19701 frgpuplem 19718 lspsn 20875 mpfind 22040 pf1ind 22261 eltg 22847 eltg2 22848 islocfin 23408 fbssfi 23728 nosupres 27627 nosupbnd1lem3 27630 nosupbnd1lem5 27632 noinffv 27641 noinfres 27642 noinfbnd1lem3 27645 noinfbnd1lem5 27647 isewlk 29403 elabreximd 32291 abfmpunirn 32421 fmlafvel 34931 isfmlasuc 34934 poimirlem3 37031 poimirlem25 37053 islshpkrN 38529 sticksstones8 41557 sticksstones9 41558 sticksstones11 41560 sticksstones17 41567 sticksstones18 41568 sn-iotalem 41629 setindtrs 42368 frege55lem1c 43269 nzss 43677 afvelrnb 46466 afvelrnb0 46467 dfatco 46559 elsetpreimafvb 46647 isgrim 47089 setis 48052 |
Copyright terms: Public domain | W3C validator |