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

Theorem elrabf 3581
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 3429 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3429 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 474 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3126 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2898 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2982 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 2002 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2894 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 624 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3567 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14syl5bb 275 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 370 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1656  wnf 1882  wcel 2164  {cab 2811  wnfc 2956  {crab 3121  Vcvv 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416
This theorem is referenced by:  rabtru  3582  elrabOLD  3586  invdisjrab  4860  rabxfrd  5117  f1ossf1o  6645  onminsb  7260  nnawordex  7984  tskwe  9089  rabssnn0fi  13080  iundisj  23714  iundisjf  29938  iundisjfi  30091  bnj1388  31636  sltval2  32337  phpreu  33929  poimirlem26  33972  rfcnpre3  40003  rfcnpre4  40004  uzwo4  40031  disjinfi  40181  allbutfiinf  40435  fsumiunss  40595  fnlimfvre  40694  stoweidlem26  41030  stoweidlem27  41031  stoweidlem31  41035  stoweidlem34  41038  stoweidlem51  41055  stoweidlem52  41056  stoweidlem59  41063  fourierdlem20  41131  fourierdlem79  41189  pimdecfgtioc  41712  smfpimcclem  41800  prmdvdsfmtnof1lem1  42319
  Copyright terms: Public domain W3C validator