Theorem elab2 3636

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1554   ∈ wcel 2136  {cab 2734  Vcvv 3448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831

This theorem is referenced by:  elint  4905  opabidw  5488  opabid  5489  oprabidw  7416  oprabid  7417  soseq  8127  tfrlem3a  8335  fsetfcdm  8830  cardprclem  9927  iunfictbso  10060  aceq3lem  10066  dfac5lem4  10072  dfac5lem4OLD  10074  kmlem9  10105  domtriomlem  10389  ltexprlem3  10986  ltexprlem4  10987  reclem2pr  10996  reclem3pr  10997  supsrlem  11059  supaddc  12149  supadd  12150  supmul1  12151  supmullem1  12152  supmullem2  12153  supmul  12154  01sqrexlem6  15250  infcvgaux2i  15864  mertenslem1  15890  mertenslem2  15891  4sqlem12  16968  conjnmzb  19269  sylow3lem2  19644  mdetunilem9  22653  txuni2  23598  xkoopn  23622  met2ndci  24555  2sqlem8  27460  2sqlem11  27463  madef  27899  eulerpartlemt  34622  eulerpartlemr  34625  eulerpartlemn  34632  subfacp1lem3  35480  subfacp1lem5  35482  dfttc4lem1  36836  dfttc4lem2  36837  rdgssun  37820  finxpsuclem  37839  heiborlem1  38258  heiborlem6  38263  heiborlem8  38265  cllem0  44090  brpermmodel  45527  fsetsnf  47593  fsetsnfo  47595  cfsetsnfsetf  47600  cfsetsnfsetf1  47601  cfsetsnfsetfo  47602