Theorem elabg 3665

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 3658	. 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  3667  elab2g  3669  elabd  3670  elab3g  3674  sbcieg  3816  intmin3  4979  finds  7884  elfi  9404  inficl  9416  dffi3  9422  scott0  9877  elgch  10613  nqpr  11005  hashf1lem1  14411  hashf1lem1OLD  14412  cshword  14737  trclublem  14938  cotrtrclfv  14955  dfiso2  17715  efgcpbllemb  19616  frgpuplem  19633  lspsn  20601  mpfind  21652  pf1ind  21856  eltg  22442  eltg2  22443  islocfin  23003  fbssfi  23323  nosupres  27190  nosupbnd1lem3  27193  nosupbnd1lem5  27195  noinffv  27204  noinfres  27205  noinfbnd1lem3  27208  noinfbnd1lem5  27210  isewlk  28839  elabreximd  31725  abfmpunirn  31855  fmlafvel  34314  isfmlasuc  34317  poimirlem3  36429  poimirlem25  36451  islshpkrN  37928  sticksstones8  40907  sticksstones9  40908  sticksstones11  40910  sticksstones17  40917  sticksstones18  40918  sn-iotalem  40986  setindtrs  41697  frege55lem1c  42600  nzss  43009  elabrexg  43661  afvelrnb  45806  afvelrnb0  45807  dfatco  45899  elsetpreimafvb  45987  setis  47645