Theorem elab2 3639

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  Vcvv 3442

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  opabidw  5480  opabid  5481  oprabidw  7399  oprabid  7400  soseq  8111  tfrlem3a  8318  fsetfcdm  8809  cardprclem  9903  iunfictbso  10036  aceq3lem  10042  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem9  10081  domtriomlem  10364  ltexprlem3  10961  ltexprlem4  10962  reclem2pr  10971  reclem3pr  10972  supsrlem  11034  supaddc  12121  supadd  12122  supmul1  12123  supmullem1  12124  supmullem2  12125  supmul  12126  01sqrexlem6  15182  infcvgaux2i  15793  mertenslem1  15819  mertenslem2  15820  4sqlem12  16896  conjnmzb  19194  sylow3lem2  19569  mdetunilem9  22576  txuni2  23521  xkoopn  23545  met2ndci  24478  2sqlem8  27405  2sqlem11  27408  madef  27844  eulerpartlemt  34548  eulerpartlemr  34551  eulerpartlemn  34558  subfacp1lem3  35395  subfacp1lem5  35397  rdgssun  37622  finxpsuclem  37641  heiborlem1  38051  heiborlem6  38056  heiborlem8  38058  cllem0  43911  brpermmodel  45348  fsetsnf  47400  fsetsnfo  47402  cfsetsnfsetf  47407  cfsetsnfsetf1  47408  cfsetsnfsetfo  47409