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

Step	Hyp	Ref	Expression
1		dfopif 4214	. 2
2		nfop.1	. . . . 5
3	2	nfel1 2635	. . . 4
4		nfop.2	. . . . 5
5	4	nfel1 2635	. . . 4
6	3, 5	nfan 1928	. . 3
7	2	nfsn 4087	. . . 4
8	2, 4	nfpr 4076	. . . 4
9	7, 8	nfpr 4076	. . 3
10		nfcv 2619	. . 3
11	6, 9, 10	nfif 3970	. 2
12	1, 11	nfcxfr 2617	1

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