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

Theorem elrabf 3348
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 3202 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3202 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 481 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 df-rab 2917 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
54eleq2i 2690 . . 3 (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)})
6 elrabf.1 . . . 4 𝑥𝐴
7 elrabf.2 . . . . . 6 𝑥𝐵
86, 7nfel 2773 . . . . 5 𝑥 𝐴𝐵
9 elrabf.3 . . . . 5 𝑥𝜓
108, 9nfan 1825 . . . 4 𝑥(𝐴𝐵𝜓)
11 eleq1 2686 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
12 elrabf.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
1311, 12anbi12d 746 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
146, 10, 13elabgf 3336 . . 3 (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥𝐵𝜑)} ↔ (𝐴𝐵𝜓)))
155, 14syl5bb 272 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
161, 3, 15pm5.21nii 368 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wnf 1705  wcel 1987  {cab 2607  wnfc 2748  {crab 2912  Vcvv 3190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192
This theorem is referenced by:  rabtru  3349  elrab  3351  rabasiun  4496  invdisjrab  4612  rabxfrd  4859  onminsb  6961  nnawordex  7677  tskwe  8736  rabssnn0fi  12741  iundisj  23256  iundisjf  29288  iundisjfi  29438  bnj1388  30862  sltval2  31563  nobndlem5  31612  phpreu  33064  poimirlem26  33106  rfcnpre3  38714  rfcnpre4  38715  uzwo4  38743  disjinfi  38889  allbutfiinf  39146  fsumiunss  39243  fnlimfvre  39342  stoweidlem26  39580  stoweidlem27  39581  stoweidlem31  39585  stoweidlem34  39588  stoweidlem51  39605  stoweidlem52  39606  stoweidlem59  39613  fourierdlem20  39681  fourierdlem79  39739  pimdecfgtioc  40262  smfpimcclem  40350  prmdvdsfmtnof1lem1  40825
  Copyright terms: Public domain W3C validator