Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  tfrlem3a Unicode version

Theorem tfrlem3a 6216
 Description: Lemma for transfinite recursion. Let be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in for later use. (Contributed by NM, 9-Apr-1995.)
Hypotheses
Ref Expression
tfrlem3.1
tfrlem3.2
Assertion
Ref Expression
tfrlem3a
Distinct variable groups:   ,,,,,   ,,,,,
Allowed substitution hints:   (,,,,)

Proof of Theorem tfrlem3a
StepHypRef Expression
1 tfrlem3.2 . 2
2 fneq12 5225 . . . 4
3 simpll 519 . . . . . . 7
4 simpr 109 . . . . . . 7
53, 4fveq12d 5437 . . . . . 6
63, 4reseq12d 4829 . . . . . . 7
76fveq2d 5434 . . . . . 6
85, 7eqeq12d 2155 . . . . 5
9 simpr 109 . . . . . 6
109adantr 274 . . . . 5
118, 10cbvraldva2 2665 . . . 4
122, 11anbi12d 465 . . 3
1312cbvrexdva 2668 . 2
14 tfrlem3.1 . 2
151, 13, 14elab2 2837 1
 Colors of variables: wff set class Syntax hints:   wa 103   wb 104   wceq 1332   wcel 1481  cab 2126  wral 2417  wrex 2418  cvv 2690  con0 4294   cres 4550   wfn 5127  cfv 5132 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2692  df-un 3081  df-in 3083  df-ss 3090  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-res 4560  df-iota 5097  df-fun 5134  df-fn 5135  df-fv 5140 This theorem is referenced by:  tfrlem3  6217  tfrlem5  6220  tfrlemisucaccv  6231  tfrlemibxssdm  6233  tfrlemi14d  6239  tfrexlem  6240
 Copyright terms: Public domain W3C validator