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

Theorem elrabf 3680
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 3518 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3518 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 481 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3152 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2909 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2997 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1893 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2905 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 630 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3668 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14syl5bb 284 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 380 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wnf 1777  wcel 2107  {cab 2804  wnfc 2966  {crab 3147  Vcvv 3500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502
This theorem is referenced by:  rabtru  3681  invdisjrabw  5048  invdisjrab  5049  rabxfrd  5314  f1ossf1o  6886  onminsb  7502  nnawordex  8253  tskwe  9368  rabssnn0fi  13344  iundisj  24064  iundisjf  30254  iundisjfi  30432  bnj1388  32189  sltval2  33047  phpreu  34743  poimirlem26  34785  rfcnpre3  41155  rfcnpre4  41156  uzwo4  41180  disjinfi  41319  allbutfiinf  41559  fsumiunss  41721  fnlimfvre  41820  stoweidlem26  42177  stoweidlem27  42178  stoweidlem31  42182  stoweidlem34  42185  stoweidlem51  42202  stoweidlem52  42203  stoweidlem59  42210  fourierdlem20  42278  fourierdlem79  42336  pimdecfgtioc  42859  smfpimcclem  42947  prmdvdsfmtnof1lem1  43578
  Copyright terms: Public domain W3C validator