Theorem elabg 3660

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 2377. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2142, ax-11 2158, ax-12 2178. (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 3653	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
2		elabg.1	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 271	. . . . 5 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
4	3	albii 1819	. . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
5		19.23v 1942	. . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
6	4, 5	bitri 275	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
7		elisset 2817	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
8		pm5.5 361	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
9	7, 8	syl 17	. . 3 ⊢ (𝐴 ∈ 𝑉 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
10	6, 9	bitrid 283	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
11	1, 10	bitrd 279	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810

This theorem is referenced by:  elab  3663  elab2g  3664  elabd  3665  elab3g  3669  sbcieg  3810  intmin3  4957  elabrexg  7240  finds  7897  elfi  9430  inficl  9442  dffi3  9448  scott0  9905  elgch  10641  nqpr  11033  hashf1lem1  14478  cshword  14814  trclublem  15019  cotrtrclfv  15036  dfiso2  17790  efgcpbllemb  19741  frgpuplem  19758  lspsn  20964  mpfind  22070  pf1ind  22298  eltg  22900  eltg2  22901  islocfin  23460  fbssfi  23780  nosupres  27676  nosupbnd1lem3  27679  nosupbnd1lem5  27681  noinffv  27690  noinfres  27691  noinfbnd1lem3  27694  noinfbnd1lem5  27696  isewlk  29587  elabreximd  32496  abfmpunirn  32635  ellpi  33393  fmlafvel  35412  isfmlasuc  35415  r1peuqusdeg1  35670  poimirlem3  37652  poimirlem25  37674  islshpkrN  39143  sticksstones8  42171  sticksstones9  42172  sticksstones11  42174  sticksstones17  42181  sticksstones18  42182  rhmqusspan  42203  sn-iotalem  42239  setindtrs  43016  frege55lem1c  43907  nzss  44308  afvelrnb  47159  afvelrnb0  47160  dfatco  47252  elsetpreimafvb  47365  isgrim  47862  isgrlim  47961  discsntermlem  49414  basrestermcfolem  49415  setis  49529