Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  wfrdmcl Structured version   Unicode version

Theorem wfrdmcl 7044
 Description: Given wrecs , then its predecessor class is a subset of . (Contributed by Scott Fenton, 21-Apr-2011.)
Hypothesis
Ref Expression
wfrlem6.1 wrecs
Assertion
Ref Expression
wfrdmcl

Proof of Theorem wfrdmcl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wfrlem6.1 . . . . . . . 8 wrecs
2 df-wrecs 7028 . . . . . . . 8 wrecs
31, 2eqtri 2449 . . . . . . 7
43dmeqi 5048 . . . . . 6
5 dmuni 5056 . . . . . 6
64, 5eqtri 2449 . . . . 5
76eleq2i 2498 . . . 4
8 eliun 4298 . . . 4
97, 8bitri 252 . . 3
10 eqid 2420 . . . . . . . 8
1110wfrlem1 7035 . . . . . . 7
1211abeq2i 2547 . . . . . 6
13 predeq3 5395 . . . . . . . . . . . . 13
1413sseq1d 3488 . . . . . . . . . . . 12
1514rspccv 3176 . . . . . . . . . . 11
1615adantl 467 . . . . . . . . . 10
17 fndm 5685 . . . . . . . . . . . . 13
1817eleq2d 2490 . . . . . . . . . . . 12
1917sseq2d 3489 . . . . . . . . . . . 12
2018, 19imbi12d 321 . . . . . . . . . . 11
2120adantr 466 . . . . . . . . . 10
2216, 21mpbird 235 . . . . . . . . 9
2322adantrl 720 . . . . . . . 8
24233adant3 1025 . . . . . . 7
2524exlimiv 1766 . . . . . 6
2612, 25sylbi 198 . . . . 5
2726reximia 2889 . . . 4
28 ssiun 4335 . . . 4
2927, 28syl 17 . . 3
309, 29sylbi 198 . 2
3130, 6syl6sseqr 3508 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437  wex 1659   wcel 1867  cab 2405  wral 2773  wrex 2774   wss 3433  cuni 4213  ciun 4293   cdm 4846   cres 4848  cpred 5390   wfn 5588  cfv 5593  wrecscwrecs 7027 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4477  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-pred 5391  df-iota 5557  df-fun 5595  df-fn 5596  df-fv 5601  df-wrecs 7028 This theorem is referenced by:  wfrlem10  7045  wfrlem14  7049  wfrlem15  7050
 Copyright terms: Public domain W3C validator