Theorem elrabf 3620

Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.)

Hypotheses

Ref	Expression
elrabf.1	⊢ Ⅎ𝑥𝐴
elrabf.2	⊢ Ⅎ𝑥𝐵
elrabf.3	⊢ Ⅎ𝑥𝜓
elrabf.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elrabf	⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Proof of Theorem elrabf

Step	Hyp	Ref	Expression
1		elex 3450	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3450	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 481	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V)
4		df-rab 3073	. . . 4 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
5	4	eleq2i 2830	. . 3 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)})
6		elrabf.1	. . . 4 ⊢ Ⅎ𝑥𝐴
7		elrabf.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
8	6, 7	nfel 2921	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
9		elrabf.3	. . . . 5 ⊢ Ⅎ𝑥𝜓
10	8, 9	nfan 1902	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓)
11		eleq1 2826	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
12		elrabf.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
13	11, 12	anbi12d 631	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
14	6, 10, 13	elabgf 3605	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
15	5, 14	bitrid 282	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
16	1, 3, 15	pm5.21nii 380	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  Ⅎwnf 1786   ∈ wcel 2106  {cab 2715  Ⅎwnfc 2887  {crab 3068  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-rab 3073  df-v 3434

This theorem is referenced by:  rabtru  3621  invdisjrabw  5059  invdisjrab  5060  rabxfrd  5340  f1ossf1o  7000  onminsb  7644  nnawordex  8468  tskwe  9708  rabssnn0fi  13706  iundisj  24712  iundisjf  30928  iundisjfi  31117  bnj1388  33013  sltval2  33859  phpreu  35761  poimirlem26  35803  sticksstones1  40102  rfcnpre3  42576  rfcnpre4  42577  uzwo4  42601  disjinfi  42731  allbutfiinf  42960  fsumiunss  43116  fnlimfvre  43215  stoweidlem26  43567  stoweidlem27  43568  stoweidlem31  43572  stoweidlem34  43575  stoweidlem51  43592  stoweidlem52  43593  stoweidlem59  43600  fourierdlem20  43668  fourierdlem79  43726  pimdecfgtioc  44252  smfpimcclem  44340  prmdvdsfmtnof1lem1  45036