Theorem elab2 3644

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  {cab 2743  Vcvv 3457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840

This theorem is referenced by:  elint  4914  opabidw  5499  opabid  5500  oprabidw  7431  oprabid  7432  soseq  8143  tfrlem3a  8351  fsetfcdm  8845  cardprclem  9953  iunfictbso  10086  aceq3lem  10092  dfac5lem4  10098  kmlem9  10130  domtriomlem  10414  ltexprlem3  11011  ltexprlem4  11012  reclem2pr  11021  reclem3pr  11022  supsrlem  11084  supaddc  12173  supadd  12174  supmul1  12175  supmullem1  12176  supmullem2  12177  supmul  12178  01sqrexlem6  15288  infcvgaux2i  15902  mertenslem1  15928  mertenslem2  15929  4sqlem12  17006  conjnmzb  19314  sylow3lem2  19689  mdetunilem9  22738  txuni2  23683  xkoopn  23707  met2ndci  24640  2sqlem8  27548  2sqlem11  27551  madef  27987  eulerpartlemt  34678  eulerpartlemr  34681  eulerpartlemn  34688  subfacp1lem3  35545  subfacp1lem5  35547  dfttc4lem1  36901  dfttc4lem2  36902  rdgssun  37884  finxpsuclem  37903  heiborlem1  38322  heiborlem6  38327  heiborlem8  38329  cllem0  44154  brpermmodel  45577  fsetsnf  47643  fsetsnfo  47645  cfsetsnfsetf  47650  cfsetsnfsetf1  47651  cfsetsnfsetfo  47652