Theorem elabg 3600

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 2139, ax-11 2156, ax-12 2173. (Revised by SN, 5-Oct-2024.)

Hypothesis

Ref	Expression
elabg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elabg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem elabg

Step	Hyp	Ref	Expression
1		elab6g 3593	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
2		elabg.1	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 270	. . . . 5 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
4	3	albii 1823	. . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
5		19.23v 1946	. . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
6	4, 5	bitri 274	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
7		elisset 2820	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
8		pm5.5 361	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
9	7, 8	syl 17	. . 3 ⊢ (𝐴 ∈ 𝑉 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
10	6, 9	syl5bb 282	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
11	1, 10	bitrd 278	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817

This theorem is referenced by:  elab  3602  elab2g  3604  elabd  3605  elab3g  3609  sbcieg  3751  intmin3  4904  finds  7719  elfi  9102  inficl  9114  dffi3  9120  scott0  9575  elgch  10309  nqpr  10701  hashf1lem1  14096  hashf1lem1OLD  14097  cshword  14432  trclublem  14634  cotrtrclfv  14651  dfiso2  17401  efgcpbllemb  19276  frgpuplem  19293  lspsn  20179  mpfind  21227  pf1ind  21431  eltg  22015  eltg2  22016  islocfin  22576  fbssfi  22896  isewlk  27872  elabreximd  30756  abfmpunirn  30891  fmlafvel  33247  isfmlasuc  33250  nosupres  33837  nosupbnd1lem3  33840  nosupbnd1lem5  33842  noinffv  33851  noinfres  33852  noinfbnd1lem3  33855  noinfbnd1lem5  33857  poimirlem3  35707  poimirlem25  35729  islshpkrN  37061  sticksstones8  40037  sticksstones9  40038  sticksstones11  40040  sticksstones17  40047  sticksstones18  40048  sn-iotalem  40117  mhphf  40208  setindtrs  40763  frege55lem1c  41413  nzss  41824  elabrexg  42478  afvelrnb  44542  afvelrnb0  44543  dfatco  44635  elsetpreimafvb  44724  setis  46289