MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrabf Structured version   Visualization version   GIF version

Theorem elrabf 3358
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
StepHypRef Expression
1 elex 3210 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3210 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 481 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 2920 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2692 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2776 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1827 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2688 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 747 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3346 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14syl5bb 272 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 368 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1482  wnf 1707  wcel 1989  {cab 2607  wnfc 2750  {crab 2915  Vcvv 3198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920  df-v 3200
This theorem is referenced by:  rabtru  3359  elrab  3361  invdisjrab  4637  rabxfrd  4887  onminsb  6996  nnawordex  7714  tskwe  8773  rabssnn0fi  12780  iundisj  23310  iundisjf  29386  iundisjfi  29540  bnj1388  31086  sltval2  31793  phpreu  33373  poimirlem26  33415  rfcnpre3  39018  rfcnpre4  39019  uzwo4  39047  disjinfi  39202  allbutfiinf  39466  fsumiunss  39613  fnlimfvre  39712  stoweidlem26  40012  stoweidlem27  40013  stoweidlem31  40017  stoweidlem34  40020  stoweidlem51  40037  stoweidlem52  40038  stoweidlem59  40045  fourierdlem20  40113  fourierdlem79  40171  pimdecfgtioc  40694  smfpimcclem  40782  prmdvdsfmtnof1lem1  41267
  Copyright terms: Public domain W3C validator