Theorem elab2 3626

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

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

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  5470  opabid  5471  oprabidw  7389  oprabid  7390  soseq  8100  tfrlem3a  8307  fsetfcdm  8798  cardprclem  9892  iunfictbso  10025  aceq3lem  10031  dfac5lem4  10037  dfac5lem4OLD  10039  kmlem9  10070  domtriomlem  10353  ltexprlem3  10950  ltexprlem4  10951  reclem2pr  10960  reclem3pr  10961  supsrlem  11023  supaddc  12112  supadd  12113  supmul1  12114  supmullem1  12115  supmullem2  12116  supmul  12117  01sqrexlem6  15198  infcvgaux2i  15812  mertenslem1  15838  mertenslem2  15839  4sqlem12  16916  conjnmzb  19217  sylow3lem2  19592  mdetunilem9  22594  txuni2  23539  xkoopn  23563  met2ndci  24496  2sqlem8  27408  2sqlem11  27411  madef  27847  eulerpartlemt  34536  eulerpartlemr  34539  eulerpartlemn  34546  subfacp1lem3  35385  subfacp1lem5  35387  dfttc4lem1  36731  dfttc4lem2  36732  rdgssun  37705  finxpsuclem  37724  heiborlem1  38143  heiborlem6  38148  heiborlem8  38150  cllem0  44008  brpermmodel  45445  fsetsnf  47496  fsetsnfo  47498  cfsetsnfsetf  47503  cfsetsnfsetf1  47504  cfsetsnfsetfo  47505