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

Theorem elrabf 3688
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 3501 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3501 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 480 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3437 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2833 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2920 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1899 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2829 . . . . 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 1540  wnf 1783  wcel 2108  {cab 2714  wnfc 2890  {crab 3436  Vcvv 3480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437  df-v 3482
This theorem is referenced by:  rabtru  3689  invdisjrab  5130  rabxfrd  5417  f1ossf1o  7148  onminsb  7814  nnawordex  8675  tskwe  9990  rabssnn0fi  14027  iundisj  25583  sltval2  27701  iundisjf  32602  iundisjfi  32798  bnj1388  35047  phpreu  37611  poimirlem26  37653  sticksstones1  42147  rfcnpre3  45038  rfcnpre4  45039  uzwo4  45058  disjinfi  45197  allbutfiinf  45431  fsumiunss  45590  fnlimfvre  45689  stoweidlem26  46041  stoweidlem27  46042  stoweidlem31  46046  stoweidlem34  46049  stoweidlem51  46066  stoweidlem52  46067  stoweidlem59  46074  fourierdlem20  46142  fourierdlem79  46200  pimdecfgtioc  46730  smfpimcclem  46822  prmdvdsfmtnof1lem1  47571
  Copyright terms: Public domain W3C validator