Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frrlem5b Structured version   Unicode version

Theorem frrlem5b 27918
 Description: Lemma for founded recursion. The union of a subclass of is a relationship. (Contributed by Paul Chapman, 29-Apr-2012.)
Hypotheses
Ref Expression
frrlem5.1
frrlem5.2 Se
frrlem5.3
Assertion
Ref Expression
frrlem5b
Distinct variable groups:   ,,,   ,,,   ,,,   ,
Allowed substitution hints:   (,)   (,,)

Proof of Theorem frrlem5b
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssel 3459 . . . 4
2 frrlem5.3 . . . . . 6
32frrlem2 27914 . . . . 5
4 funrel 5544 . . . . 5
53, 4syl 16 . . . 4
61, 5syl6 33 . . 3
76ralrimiv 2828 . 2
8 reluni 5071 . 2
97, 8sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 965   wceq 1370  wex 1587   wcel 1758  cab 2439  wral 2799   wss 3437  cuni 4200   wfr 4785   Se wse 4786   cres 4951   wrel 4954   wfun 5521   wfn 5522  cfv 5527  (class class class)co 6201  cpred 27769 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-fv 5535  df-ov 6204  df-pred 27770 This theorem is referenced by:  frrlem5c  27919
 Copyright terms: Public domain W3C validator