Theorem elab2 3627

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {cab 2718  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815

This theorem is referenced by:  elint  4890  opabidw  5473  opabid  5474  oprabidw  7394  oprabid  7395  soseq  8106  tfrlem3a  8313  fsetfcdm  8804  cardprclem  9901  iunfictbso  10034  aceq3lem  10040  dfac5lem4  10046  dfac5lem4OLD  10048  kmlem9  10079  domtriomlem  10362  ltexprlem3  10959  ltexprlem4  10960  reclem2pr  10969  reclem3pr  10970  supsrlem  11032  supaddc  12121  supadd  12122  supmul1  12123  supmullem1  12124  supmullem2  12125  supmul  12126  01sqrexlem6  15207  infcvgaux2i  15821  mertenslem1  15847  mertenslem2  15848  4sqlem12  16925  conjnmzb  19226  sylow3lem2  19601  mdetunilem9  22610  txuni2  23555  xkoopn  23579  met2ndci  24512  2sqlem8  27414  2sqlem11  27417  madef  27853  eulerpartlemt  34562  eulerpartlemr  34565  eulerpartlemn  34572  subfacp1lem3  35411  subfacp1lem5  35413  dfttc4lem1  36757  dfttc4lem2  36758  rdgssun  37741  finxpsuclem  37760  heiborlem1  38179  heiborlem6  38184  heiborlem8  38186  cllem0  44011  brpermmodel  45448  fsetsnf  47515  fsetsnfo  47517  cfsetsnfsetf  47522  cfsetsnfsetf1  47523  cfsetsnfsetfo  47524