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

Theorem nfop 4233
Description: Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
Hypotheses
Ref Expression
nfop.1
nfop.2
Assertion
Ref Expression
nfop

Proof of Theorem nfop
StepHypRef Expression
1 dfopif 4214 . 2
2 nfop.1 . . . . 5
32nfel1 2635 . . . 4
4 nfop.2 . . . . 5
54nfel1 2635 . . . 4
63, 5nfan 1928 . . 3
72nfsn 4087 . . . 4
82, 4nfpr 4076 . . . 4
97, 8nfpr 4076 . . 3
10 nfcv 2619 . . 3
116, 9, 10nfif 3970 . 2
121, 11nfcxfr 2617 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  e.wcel 1818  F/_wnfc 2605   cvv 3109   c0 3784  ifcif 3941  {csn 4029  {cpr 4031  <.cop 4035
This theorem is referenced by:  nfopd  4234  csbopg  4235  moop2  4747  fliftfuns  6212  dfmpt2  6890  qliftfuns  7417  xpf1o  7699  nfseq  12117  txcnp  20121  cnmpt1t  20166  cnmpt2t  20174  flfcnp2  20508  nfaov  32264  bnj958  33998  bnj1000  33999  bnj1446  34101  bnj1447  34102  bnj1448  34103  bnj1466  34109  bnj1467  34110  bnj1519  34121  bnj1520  34122  bnj1529  34126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036
  Copyright terms: Public domain W3C validator