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

Theorem wfrdmss 7047
 Description: The domain of the well-founded recursion generator is a subclass of . (Contributed by Scott Fenton, 21-Apr-2011.)
Hypothesis
Ref Expression
wfrlem6.1 wrecs
Assertion
Ref Expression
wfrdmss

Proof of Theorem wfrdmss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wfrlem6.1 . . . . 5 wrecs
2 df-wrecs 7033 . . . . 5 wrecs
31, 2eqtri 2451 . . . 4
43dmeqi 5052 . . 3
5 dmuni 5060 . . 3
64, 5eqtri 2451 . 2
7 iunss 4337 . . 3
8 eqid 2422 . . . 4
98wfrlem3 7042 . . 3
107, 9mprgbir 2789 . 2
116, 10eqsstri 3494 1
 Colors of variables: wff setvar class Syntax hints:   wa 370   w3a 982   wceq 1437  wex 1659  cab 2407  wral 2775   wss 3436  cuni 4216  ciun 4296   cdm 4850   cres 4852  cpred 5395   wfn 5593  cfv 5598  wrecscwrecs 7032 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 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400 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 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-iota 5562  df-fun 5600  df-fn 5601  df-fv 5606  df-wrecs 7033 This theorem is referenced by:  wfrlem8  7048  wfrlem10  7050  wfrlem15  7055  wfrlem16  7056
 Copyright terms: Public domain W3C validator