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

Theorem elrabf 3584
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 3416 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3416 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 484 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 3062 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2824 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2913 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1906 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2820 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 634 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3568 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14syl5bb 286 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 383 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wnf 1790  wcel 2114  {cab 2716  wnfc 2879  {crab 3057  Vcvv 3398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-rab 3062  df-v 3400
This theorem is referenced by:  rabtru  3585  invdisjrabw  5015  invdisjrab  5016  rabxfrd  5284  f1ossf1o  6900  onminsb  7533  nnawordex  8294  tskwe  9452  rabssnn0fi  13445  iundisj  24300  iundisjf  30502  iundisjfi  30692  bnj1388  32584  sltval2  33500  phpreu  35384  poimirlem26  35426  sticksstones1  39708  rfcnpre3  42114  rfcnpre4  42115  uzwo4  42139  disjinfi  42269  allbutfiinf  42498  fsumiunss  42658  fnlimfvre  42757  stoweidlem26  43109  stoweidlem27  43110  stoweidlem31  43114  stoweidlem34  43117  stoweidlem51  43134  stoweidlem52  43135  stoweidlem59  43142  fourierdlem20  43210  fourierdlem79  43268  pimdecfgtioc  43791  smfpimcclem  43879  prmdvdsfmtnof1lem1  44570
  Copyright terms: Public domain W3C validator