Theorem elab2 3640

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)

Hypotheses

Ref	Expression
elab2.1	⊢ 𝐴 ∈ V
elab2.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
elab2.3	⊢ 𝐵 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
elab2	⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

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

Proof of Theorem elab2

Step	Hyp	Ref	Expression
1		elab2.1	. 2 ⊢ 𝐴 ∈ V
2		elab2.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elab2.3	. . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑}
4	2, 3	elab2g 3638	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓))
5	1, 4	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  Vcvv 3438

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  opabidw  5471  opabid  5472  oprabidw  7384  oprabid  7385  soseq  8099  tfrlem3a  8306  fsetfcdm  8794  cardprclem  9894  iunfictbso  10027  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem9  10072  domtriomlem  10355  ltexprlem3  10951  ltexprlem4  10952  reclem2pr  10961  reclem3pr  10962  supsrlem  11024  supaddc  12110  supadd  12111  supmul1  12112  supmullem1  12113  supmullem2  12114  supmul  12115  01sqrexlem6  15172  infcvgaux2i  15783  mertenslem1  15809  mertenslem2  15810  4sqlem12  16886  conjnmzb  19150  sylow3lem2  19525  mdetunilem9  22523  txuni2  23468  xkoopn  23492  met2ndci  24426  2sqlem8  27353  2sqlem11  27356  madef  27784  eulerpartlemt  34338  eulerpartlemr  34341  eulerpartlemn  34348  subfacp1lem3  35154  subfacp1lem5  35156  rdgssun  37351  finxpsuclem  37370  heiborlem1  37790  heiborlem6  37795  heiborlem8  37797  cllem0  43539  brpermmodel  44977  fsetsnf  47036  fsetsnfo  47038  cfsetsnfsetf  47043  cfsetsnfsetf1  47044  cfsetsnfsetfo  47045