Theorem elab2 3640

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ∈ wcel 2141  {cab 2739  Vcvv 3453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is referenced by:  elint  4917  opabidw  5508  opabid  5509  oprabidw  7441  oprabid  7442  soseq  8154  tfrlem3a  8362  fsetfcdm  8856  cardprclem  9964  iunfictbso  10097  aceq3lem  10103  dfac5lem4  10109  kmlem9  10141  domtriomlem  10425  ltexprlem3  11022  ltexprlem4  11023  reclem2pr  11032  reclem3pr  11033  supsrlem  11095  supaddc  12181  supadd  12182  supmul1  12183  supmullem1  12184  supmullem2  12185  supmul  12186  01sqrexlem6  15298  infcvgaux2i  15912  mertenslem1  15938  mertenslem2  15939  4sqlem12  17015  conjnmzb  19322  sylow3lem2  19697  mdetunilem9  22756  txuni2  23701  xkoopn  23725  met2ndci  24658  2sqlem8  27566  2sqlem11  27569  madef  28005  eulerpartlemt  34727  eulerpartlemr  34730  eulerpartlemn  34737  subfacp1lem3  35640  subfacp1lem5  35642  dfttc4lem1  37005  dfttc4lem2  37006  rdgssun  37990  finxpsuclem  38009  heiborlem1  38428  heiborlem6  38433  heiborlem8  38435  cllem0  44262  brpermmodel  45682  fsetsnf  47755  fsetsnfo  47757  cfsetsnfsetf  47762  cfsetsnfsetf1  47763  cfsetsnfsetfo  47764