Theorem elabg 3619

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 2376. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (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		elabg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	ax-gen 1797	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3614	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 692	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  elab  3622  elab2g  3623  elabd  3624  elab3g  3628  sbcieg  3768  intmin3  4918  elabrexg  7198  finds  7847  elfi  9326  inficl  9338  dffi3  9344  scott0  9810  elgch  10545  nqpr  10937  hashf1lem1  14417  cshword  14753  trclublem  14957  cotrtrclfv  14974  dfiso2  17739  efgcpbllemb  19730  frgpuplem  19747  lspsn  20997  mpfind  22093  pf1ind  22320  eltg  22922  eltg2  22923  islocfin  23482  fbssfi  23802  nosupres  27671  nosupbnd1lem3  27674  nosupbnd1lem5  27676  noinffv  27685  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  isewlk  29671  elabreximd  32580  abfmpunirn  32725  ellpi  33433  fmlafvel  35567  isfmlasuc  35570  r1peuqusdeg1  35825  poimirlem3  37944  poimirlem25  37966  islshpkrN  39566  sticksstones8  42592  sticksstones9  42593  sticksstones11  42595  sticksstones17  42602  sticksstones18  42603  rhmqusspan  42624  sn-iotalem  42662  setindtrs  43453  frege55lem1c  44343  nzss  44744  afvelrnb  47611  afvelrnb0  47612  dfatco  47704  elsetpreimafvb  47844  isgrim  48358  isgrlim  48458  discsntermlem  50045  basrestermcfolem  50046  setis  50173