Theorem elabg 3667

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.)

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 3660	. 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 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

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  3669  elab2g  3671  elabd  3672  elab3g  3676  sbcieg  3818  intmin3  4981  finds  7889  elfi  9408  inficl  9420  dffi3  9426  scott0  9881  elgch  10617  nqpr  11009  hashf1lem1  14415  hashf1lem1OLD  14416  cshword  14741  trclublem  14942  cotrtrclfv  14959  dfiso2  17719  efgcpbllemb  19623  frgpuplem  19640  lspsn  20613  mpfind  21670  pf1ind  21874  eltg  22460  eltg2  22461  islocfin  23021  fbssfi  23341  nosupres  27210  nosupbnd1lem3  27213  nosupbnd1lem5  27215  noinffv  27224  noinfres  27225  noinfbnd1lem3  27228  noinfbnd1lem5  27230  isewlk  28859  elabreximd  31747  abfmpunirn  31877  fmlafvel  34376  isfmlasuc  34379  poimirlem3  36491  poimirlem25  36513  islshpkrN  37990  sticksstones8  40969  sticksstones9  40970  sticksstones11  40972  sticksstones17  40979  sticksstones18  40980  sn-iotalem  41038  setindtrs  41764  frege55lem1c  42667  nzss  43076  elabrexg  43728  afvelrnb  45871  afvelrnb0  45872  dfatco  45964  elsetpreimafvb  46052  setis  47743