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

Theorem elrabf 3679
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 3492 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3492 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 480 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3432 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2824 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2916 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1901 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2820 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 630 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3664 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14bitrid 283 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 378 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1540  wnf 1784  wcel 2105  {cab 2708  wnfc 2882  {crab 3431  Vcvv 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-rab 3432  df-v 3475
This theorem is referenced by:  rabtru  3680  invdisjrabw  5133  invdisjrab  5134  rabxfrd  5415  f1ossf1o  7128  onminsb  7786  nnawordex  8643  tskwe  9951  rabssnn0fi  13958  iundisj  25397  sltval2  27502  iundisjf  32253  iundisjfi  32440  bnj1388  34508  phpreu  36936  poimirlem26  36978  sticksstones1  41429  rfcnpre3  44180  rfcnpre4  44181  uzwo4  44202  disjinfi  44350  allbutfiinf  44589  fsumiunss  44750  fnlimfvre  44849  stoweidlem26  45201  stoweidlem27  45202  stoweidlem31  45206  stoweidlem34  45209  stoweidlem51  45226  stoweidlem52  45227  stoweidlem59  45234  fourierdlem20  45302  fourierdlem79  45360  pimdecfgtioc  45890  smfpimcclem  45982  prmdvdsfmtnof1lem1  46711
  Copyright terms: Public domain W3C validator