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

Theorem elrabf 3642
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 3462 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3462 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 482 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3407 . . . 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 3627 . . 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 3406  Vcvv 3444
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 3407  df-v 3446
This theorem is referenced by:  rabtru  3643  invdisjrabw  5091  invdisjrab  5092  rabxfrd  5373  f1ossf1o  7075  onminsb  7730  nnawordex  8585  tskwe  9891  rabssnn0fi  13897  iundisj  24928  sltval2  27020  iundisjf  31553  iundisjfi  31746  bnj1388  33702  phpreu  36108  poimirlem26  36150  sticksstones1  40600  rfcnpre3  43326  rfcnpre4  43327  uzwo4  43349  disjinfi  43500  allbutfiinf  43741  fsumiunss  43902  fnlimfvre  44001  stoweidlem26  44353  stoweidlem27  44354  stoweidlem31  44358  stoweidlem34  44361  stoweidlem51  44378  stoweidlem52  44379  stoweidlem59  44386  fourierdlem20  44454  fourierdlem79  44512  pimdecfgtioc  45042  smfpimcclem  45134  prmdvdsfmtnof1lem1  45862
  Copyright terms: Public domain W3C validator