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

Theorem nfcprod 13908
 Description: Bound-variable hypothesis builder for product: if is (effectively) not free in and , it is not free in . (Contributed by Scott Fenton, 1-Dec-2017.)
Hypotheses
Ref Expression
nfcprod.1
nfcprod.2
Assertion
Ref Expression
nfcprod
Distinct variable group:   ,
Allowed substitution hints:   (,)   (,)

Proof of Theorem nfcprod
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-prod 13903 . 2
2 nfcv 2569 . . . . 5
3 nfcprod.1 . . . . . . 7
4 nfcv 2569 . . . . . . 7
53, 4nfss 3400 . . . . . 6
6 nfv 1755 . . . . . . . . 9
7 nfcv 2569 . . . . . . . . . . 11
8 nfcv 2569 . . . . . . . . . . 11
93nfcri 2563 . . . . . . . . . . . . 13
10 nfcprod.2 . . . . . . . . . . . . 13
11 nfcv 2569 . . . . . . . . . . . . 13
129, 10, 11nfif 3883 . . . . . . . . . . . 12
132, 12nfmpt 4455 . . . . . . . . . . 11
147, 8, 13nfseq 12173 . . . . . . . . . 10
15 nfcv 2569 . . . . . . . . . 10
16 nfcv 2569 . . . . . . . . . 10
1714, 15, 16nfbr 4411 . . . . . . . . 9
186, 17nfan 1988 . . . . . . . 8
1918nfex 2008 . . . . . . 7
204, 19nfrex 2827 . . . . . 6
21 nfcv 2569 . . . . . . . 8
2221, 8, 13nfseq 12173 . . . . . . 7
23 nfcv 2569 . . . . . . 7
2422, 15, 23nfbr 4411 . . . . . 6
255, 20, 24nf3an 1990 . . . . 5
262, 25nfrex 2827 . . . 4
27 nfcv 2569 . . . . 5
28 nfcv 2569 . . . . . . . 8
29 nfcv 2569 . . . . . . . 8
3028, 29, 3nff1o 5772 . . . . . . 7
31 nfcv 2569 . . . . . . . . . . . 12
3231, 10nfcsb 3356 . . . . . . . . . . 11
3327, 32nfmpt 4455 . . . . . . . . . 10
3411, 8, 33nfseq 12173 . . . . . . . . 9
3534, 21nffv 5832 . . . . . . . 8
3635nfeq2 2584 . . . . . . 7
3730, 36nfan 1988 . . . . . 6
3837nfex 2008 . . . . 5
3927, 38nfrex 2827 . . . 4
4026, 39nfor 1995 . . 3
4140nfiota 5512 . 2
421, 41nfcxfr 2567 1
 Colors of variables: wff setvar class Syntax hints:   wo 369   wa 370   w3a 982   wceq 1437  wex 1657   wcel 1872  wnfc 2556   wne 2599  wrex 2715  csb 3338   wss 3379  cif 3854   class class class wbr 4366   cmpt 4425  cio 5506  wf1o 5543  cfv 5544  (class class class)co 6249  cc0 9490  c1 9491   cmul 9495  cn 10560  cz 10888  cuz 11110  cfz 11735   cseq 12163   cli 13491  cprod 13902 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-seq 12164  df-prod 13903 This theorem is referenced by:  fprod2dlem  13977  fprodcom2  13981  fprodcncf  37662
 Copyright terms: Public domain W3C validator