Theorem elabg 3351

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.)

Hypothesis

Ref	Expression
elabg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elabg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem elabg

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1843	. 2 ⊢ Ⅎ𝑥𝜓
3		elabg.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	elabgf 3348	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990  {cab 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202

This theorem is referenced by:  elab2g  3353  intmin3  4505  elxpi  5130  finds  7092  wfrlem15  7429  elfi  8319  inficl  8331  dffi3  8337  scott0  8749  elgch  9444  nqpr  9836  hashf1lem1  13239  cshword  13537  trclublem  13734  cotrtrclfv  13753  dfiso2  16432  lubval  16984  glbval  16997  efgcpbllemb  18168  frgpuplem  18185  lspsn  19002  mpfind  19536  pf1ind  19719  eltg  20761  eltg2  20762  islocfin  21320  fbssfi  21641  isewlk  26498  elabreximd  29348  abfmpunirn  29452  orvcval  30519  nosupfv  31852  nosupres  31853  nosupbnd1lem3  31856  nosupbnd1lem5  31858  poimirlem3  33412  poimirlem25  33434  islshpkrN  34407  setindtrs  37592  rngunsnply  37743  frege55lem1c  38210  nzss  38516  elabrexg  39206  ismea  40668  afvelrnb  41243  afvelrnb0  41244  cshword2  41437