Theorem elrabf 3645

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 3475	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3475	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V)
4		df-rab 3417	. . . 4 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
5	4	eleq2i 2856	. . 3 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)})
6		elrabf.1	. . . 4 ⊢ Ⅎ𝑥𝐴
7		elrabf.2	. . . . . 6 ⊢ Ⅎ𝑥𝐵
8	6, 7	nfel 2940	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
9		elrabf.3	. . . . 5 ⊢ Ⅎ𝑥𝜓
10	8, 9	nfan 1934	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓)
11		eleq1 2852	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
12		elrabf.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
13	11, 12	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
14	6, 10, 13	elabgf 3631	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
15	5, 14	bitrid 286	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
16	1, 3, 15	pm5.21nii 381	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2147  {cab 2741  Ⅎwnfc 2911  {crab 3416  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rab 3417  df-v 3456

This theorem is used by:  rabtru  3646  invdisjrab  5095  rabxfrd  5386  f1ossf1o  7161  onminsb  7842  nnawordex  8684  tskwe  10068  rabssnn0fi  14169  iundisj  25924  ltsval2  28070  iundisjf  33281  iundisjfi  33484  bnj1388  35774  phpreu  38795  poimirlem26  38832  sticksstones1  43462  rfcnpre3  46324  rfcnpre4  46325  uzwo4  46344  disjinfi  46480  allbutfiinf  46703  fsumiunss  46860  fnlimfvre  46957  stoweidlem26  47309  stoweidlem27  47310  stoweidlem31  47314  stoweidlem34  47317  stoweidlem51  47334  stoweidlem52  47335  stoweidlem59  47342  fourierdlem20  47410  fourierdlem79  47468  pimdecfgtioc  47998  smfpimcclem  48090  prmdvdsfmtnof1lem1  48942