Theorem elab2 3635

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {cab 2711  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808

This theorem is referenced by:  opabidw  5469  opabid  5470  oprabidw  7386  oprabid  7387  soseq  8098  tfrlem3a  8305  fsetfcdm  8793  cardprclem  9882  iunfictbso  10015  aceq3lem  10021  dfac5lem4  10027  dfac5lem4OLD  10029  kmlem9  10060  domtriomlem  10343  ltexprlem3  10939  ltexprlem4  10940  reclem2pr  10949  reclem3pr  10950  supsrlem  11012  supaddc  12099  supadd  12100  supmul1  12101  supmullem1  12102  supmullem2  12103  supmul  12104  01sqrexlem6  15164  infcvgaux2i  15775  mertenslem1  15801  mertenslem2  15802  4sqlem12  16878  conjnmzb  19175  sylow3lem2  19550  mdetunilem9  22545  txuni2  23490  xkoopn  23514  met2ndci  24447  2sqlem8  27374  2sqlem11  27377  madef  27807  eulerpartlemt  34395  eulerpartlemr  34398  eulerpartlemn  34405  subfacp1lem3  35237  subfacp1lem5  35239  rdgssun  37433  finxpsuclem  37452  heiborlem1  37861  heiborlem6  37866  heiborlem8  37868  cllem0  43673  brpermmodel  45110  fsetsnf  47165  fsetsnfo  47167  cfsetsnfsetf  47172  cfsetsnfsetf1  47173  cfsetsnfsetfo  47174