Theorem elab2 3637

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 3635	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓))
5	1, 4	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {cab 2708  Vcvv 3446

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809

This theorem is referenced by:  opabidw  5486  opabid  5487  oprabidw  7393  oprabid  7394  soseq  8096  wfrlem3OLDa  8262  tfrlem3a  8328  fsetfcdm  8805  cardprclem  9924  iunfictbso  10059  aceq3lem  10065  dfac5lem4  10071  kmlem9  10103  domtriomlem  10387  ltexprlem3  10983  ltexprlem4  10984  reclem2pr  10993  reclem3pr  10994  supsrlem  11056  supaddc  12131  supadd  12132  supmul1  12133  supmullem1  12134  supmullem2  12135  supmul  12136  01sqrexlem6  15144  infcvgaux2i  15754  mertenslem1  15780  mertenslem2  15781  4sqlem12  16839  conjnmzb  19057  sylow3lem2  19424  mdetunilem9  22006  txuni2  22953  xkoopn  22977  met2ndci  23915  2sqlem8  26811  2sqlem11  26814  madef  27229  eulerpartlemt  33060  eulerpartlemr  33063  eulerpartlemn  33070  subfacp1lem3  33863  subfacp1lem5  33865  rdgssun  35922  finxpsuclem  35941  heiborlem1  36343  heiborlem6  36348  heiborlem8  36350  cllem0  41960  fsetsnf  45405  fsetsnfo  45407  cfsetsnfsetf  45412  cfsetsnfsetf1  45413  cfsetsnfsetfo  45414