Theorem elabg 3690

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 2380. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2141, 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 3682	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
2		elabg.1	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 271	. . . . 5 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
4	3	albii 1817	. . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
5		19.23v 1941	. . . 4 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
6	4, 5	bitri 275	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
7		elisset 2826	. . . 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 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819

This theorem is referenced by:  elab  3694  elab2g  3696  elabd  3697  elab3g  3701  sbcieg  3845  intmin3  5000  elabrexg  7280  finds  7936  elfi  9482  inficl  9494  dffi3  9500  scott0  9955  elgch  10691  nqpr  11083  hashf1lem1  14504  cshword  14839  trclublem  15044  cotrtrclfv  15061  dfiso2  17833  efgcpbllemb  19797  frgpuplem  19814  lspsn  21023  mpfind  22154  pf1ind  22380  eltg  22985  eltg2  22986  islocfin  23546  fbssfi  23866  nosupres  27770  nosupbnd1lem3  27773  nosupbnd1lem5  27775  noinffv  27784  noinfres  27785  noinfbnd1lem3  27788  noinfbnd1lem5  27790  isewlk  29638  elabreximd  32538  abfmpunirn  32670  ellpi  33366  fmlafvel  35353  isfmlasuc  35356  r1peuqusdeg1  35611  poimirlem3  37583  poimirlem25  37605  islshpkrN  39076  sticksstones8  42110  sticksstones9  42111  sticksstones11  42113  sticksstones17  42120  sticksstones18  42121  rhmqusspan  42142  sn-iotalem  42214  setindtrs  42982  frege55lem1c  43878  nzss  44286  afvelrnb  47078  afvelrnb0  47079  dfatco  47171  elsetpreimafvb  47258  isgrim  47752  isgrlim  47806  setis  48790