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

Theorem elrabf 3690
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 3498 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3498 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 480 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3433 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2830 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2917 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1896 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2826 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 632 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3674 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14bitrid 283 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 378 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wnf 1779  wcel 2105  {cab 2711  wnfc 2887  {crab 3432  Vcvv 3477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-rab 3433  df-v 3479
This theorem is referenced by:  rabtru  3691  invdisjrab  5134  rabxfrd  5422  f1ossf1o  7147  onminsb  7813  nnawordex  8673  tskwe  9987  rabssnn0fi  14023  iundisj  25596  sltval2  27715  iundisjf  32608  iundisjfi  32803  bnj1388  35025  phpreu  37590  poimirlem26  37632  sticksstones1  42127  rfcnpre3  44970  rfcnpre4  44971  uzwo4  44992  disjinfi  45134  allbutfiinf  45369  fsumiunss  45530  fnlimfvre  45629  stoweidlem26  45981  stoweidlem27  45982  stoweidlem31  45986  stoweidlem34  45989  stoweidlem51  46006  stoweidlem52  46007  stoweidlem59  46014  fourierdlem20  46082  fourierdlem79  46140  pimdecfgtioc  46670  smfpimcclem  46762  prmdvdsfmtnof1lem1  47508
  Copyright terms: Public domain W3C validator