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

Theorem nfseq 10258
 Description: Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
Hypotheses
Ref Expression
nfseq.1
nfseq.2
nfseq.3
Assertion
Ref Expression
nfseq

Proof of Theorem nfseq
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-seqfrec 10249 . 2 frec
2 nfcv 2282 . . . . . 6
3 nfseq.1 . . . . . 6
42, 3nffv 5438 . . . . 5
5 nfcv 2282 . . . . 5
6 nfcv 2282 . . . . . 6
7 nfcv 2282 . . . . . . 7
8 nfseq.2 . . . . . . 7
9 nfseq.3 . . . . . . . 8
109, 6nffv 5438 . . . . . . 7
117, 8, 10nfov 5808 . . . . . 6
126, 11nfop 3728 . . . . 5
134, 5, 12nfmpo 5847 . . . 4
149, 3nffv 5438 . . . . 5
153, 14nfop 3728 . . . 4
1613, 15nffrec 6300 . . 3 frec
1716nfrn 4791 . 2 frec
181, 17nfcxfr 2279 1
 Colors of variables: wff set class Syntax hints:  wnfc 2269  cvv 2689  cop 3534   crn 4547  cfv 5130  (class class class)co 5781   cmpo 5783  freccfrec 6294  c1 7644   caddc 7646  cuz 9349   cseq 10248 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-rab 2426  df-v 2691  df-un 3079  df-in 3081  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-opab 3997  df-mpt 3998  df-xp 4552  df-cnv 4554  df-dm 4556  df-rn 4557  df-res 4558  df-iota 5095  df-fv 5138  df-ov 5784  df-oprab 5785  df-mpo 5786  df-recs 6209  df-frec 6295  df-seqfrec 10249 This theorem is referenced by:  seq3f1olemstep  10304  seq3f1olemp  10305  nfsum1  11156  nfsum  11157  nfcprod1  11354  nfcprod  11355
 Copyright terms: Public domain W3C validator