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

Theorem elrabf 3488
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 3340 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3340 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 472 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3047 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2819 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2903 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1965 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2815 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 749 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3476 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14syl5bb 272 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 367 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1620  wnf 1845  wcel 2127  {cab 2734  wnfc 2877  {crab 3042  Vcvv 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-rab 3047  df-v 3330
This theorem is referenced by:  rabtru  3489  elrab  3492  invdisjrab  4779  rabxfrd  5026  onminsb  7152  nnawordex  7874  tskwe  8937  rabssnn0fi  12950  iundisj  23487  iundisjf  29680  iundisjfi  29835  bnj1388  31379  sltval2  32086  phpreu  33675  poimirlem26  33717  rfcnpre3  39660  rfcnpre4  39661  uzwo4  39689  disjinfi  39848  allbutfiinf  40114  fsumiunss  40279  fnlimfvre  40378  stoweidlem26  40715  stoweidlem27  40716  stoweidlem31  40720  stoweidlem34  40723  stoweidlem51  40740  stoweidlem52  40741  stoweidlem59  40748  fourierdlem20  40816  fourierdlem79  40874  pimdecfgtioc  41400  smfpimcclem  41488  prmdvdsfmtnof1lem1  41975
  Copyright terms: Public domain W3C validator