Theorem elab2 3495

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2140  {cab 2747  Vcvv 3341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343

This theorem is referenced by:  elpw  4309  elint  4634  opabid  5133  elrn2  5521  elimasn  5649  oprabid  6842  wfrlem3a  7588  tfrlem3a  7644  cardprclem  9016  iunfictbso  9148  aceq3lem  9154  dfac5lem4  9160  kmlem9  9193  domtriomlem  9477  ltexprlem3  10073  ltexprlem4  10074  reclem2pr  10083  reclem3pr  10084  supsrlem  10145  supaddc  11203  supadd  11204  supmul1  11205  supmullem1  11206  supmullem2  11207  supmul  11208  sqrlem6  14208  infcvgaux2i  14810  mertenslem1  14836  mertenslem2  14837  4sqlem12  15883  conjnmzb  17917  sylow3lem2  18264  mdetunilem9  20649  txuni2  21591  xkoopn  21615  met2ndci  22549  2sqlem8  25372  2sqlem11  25375  eulerpartlemt  30764  eulerpartlemr  30767  eulerpartlemn  30774  subfacp1lem3  31493  subfacp1lem5  31495  soseq  32082  finxpsuclem  33564  heiborlem1  33942  heiborlem6  33947  heiborlem8  33949  cllem0  38392