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.) |
Ref | Expression |
---|---|
elabg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elabg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1830 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | elabg.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | elabgf 3317 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∈ wcel 1977 {cab 2596 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 |
This theorem is referenced by: elab2g 3322 intmin3 4440 elxpi 5054 finds 6984 wfrlem15 7316 elfi 8202 inficl 8214 dffi3 8220 scott0 8632 elgch 9323 nqpr 9715 hashf1lem1 13096 cshword 13388 trclublem 13582 cotrtrclfv 13601 dfiso2 16255 lubval 16807 glbval 16820 efgcpbllemb 17991 frgpuplem 18008 lspsn 18823 mpfind 19357 pf1ind 19540 eltg 20572 eltg2 20573 islocfin 21130 fbssfi 21451 elabreximd 28732 abfmpunirn 28832 orvcval 29846 poimirlem3 32582 poimirlem25 32604 islshpkrN 33425 setindtrs 36610 rngunsnply 36762 frege55lem1c 37230 nzss 37538 elabrexg 38229 ismea 39344 isome 39384 afvelrnb 39892 afvelrnb0 39893 cshword2 40300 isewlk 40804 setrec1lem1 42233 |
Copyright terms: Public domain | W3C validator |