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

Theorem elrabf 3680
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 3493 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3493 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 482 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3434 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2826 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2918 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1903 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2822 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 632 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3665 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14bitrid 283 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 380 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wnf 1786  wcel 2107  {cab 2710  wnfc 2884  {crab 3433  Vcvv 3475
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434  df-v 3477
This theorem is referenced by:  rabtru  3681  invdisjrabw  5134  invdisjrab  5135  rabxfrd  5416  f1ossf1o  7126  onminsb  7782  nnawordex  8637  tskwe  9945  rabssnn0fi  13951  iundisj  25065  sltval2  27159  iundisjf  31820  iundisjfi  32007  bnj1388  34044  phpreu  36472  poimirlem26  36514  sticksstones1  40962  rfcnpre3  43717  rfcnpre4  43718  uzwo4  43740  disjinfi  43891  allbutfiinf  44130  fsumiunss  44291  fnlimfvre  44390  stoweidlem26  44742  stoweidlem27  44743  stoweidlem31  44747  stoweidlem34  44750  stoweidlem51  44767  stoweidlem52  44768  stoweidlem59  44775  fourierdlem20  44843  fourierdlem79  44901  pimdecfgtioc  45431  smfpimcclem  45523  prmdvdsfmtnof1lem1  46252
  Copyright terms: Public domain W3C validator