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

Theorem elrabf 3329
 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 3185 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3185 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 480 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 2905 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2680 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2763 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1816 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2676 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 743 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3317 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14syl5bb 271 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 367 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  Ⅎwnf 1699   ∈ wcel 1977  {cab 2596  Ⅎwnfc 2738  {crab 2900  Vcvv 3173 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175 This theorem is referenced by:  elrab  3331  rabasiun  4459  invdisjrab  4572  rabxfrd  4815  onminsb  6891  nnawordex  7604  tskwe  8659  rabssnn0fi  12647  iundisj  23123  rabtru  28723  iundisjf  28784  iundisjfi  28942  bnj1388  30355  sltval2  31053  nobndlem5  31095  phpreu  32563  poimirlem26  32605  rfcnpre3  38215  rfcnpre4  38216  uzwo4  38246  disjinfi  38375  fsumiunss  38642  fnlimfvre  38741  stoweidlem26  38919  stoweidlem27  38920  stoweidlem31  38924  stoweidlem34  38927  stoweidlem51  38944  stoweidlem52  38945  stoweidlem59  38952  fourierdlem20  39020  fourierdlem79  39078  pimdecfgtioc  39602  prmdvdsfmtnof1lem1  40034
 Copyright terms: Public domain W3C validator