Theorem elab2 3670

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  {cab 2799  Vcvv 3495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963

This theorem is referenced by:  elpwOLD  4548  elint  4875  opabidw  5405  opabid  5406  elrn2  5816  elimasn  5949  oprabidw  7181  oprabid  7182  wfrlem3a  7951  tfrlem3a  8007  cardprclem  9402  iunfictbso  9534  aceq3lem  9540  dfac5lem4  9546  kmlem9  9578  domtriomlem  9858  ltexprlem3  10454  ltexprlem4  10455  reclem2pr  10464  reclem3pr  10465  supsrlem  10527  supaddc  11602  supadd  11603  supmul1  11604  supmullem1  11605  supmullem2  11606  supmul  11607  sqrlem6  14601  infcvgaux2i  15207  mertenslem1  15234  mertenslem2  15235  4sqlem12  16286  conjnmzb  18387  sylow3lem2  18747  mdetunilem9  21223  txuni2  22167  xkoopn  22191  met2ndci  23126  2sqlem8  25996  2sqlem11  25999  eulerpartlemt  31624  eulerpartlemr  31627  eulerpartlemn  31634  subfacp1lem3  32424  subfacp1lem5  32426  soseq  33091  rdgssun  34653  finxpsuclem  34672  heiborlem1  35083  heiborlem6  35088  heiborlem8  35090  cllem0  39918