Theorem nfop 4418

Description: Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)

Hypotheses

Ref	Expression
nfop.1	|- F/_ x A
nfop.2	|- F/_ x B

Assertion

Ref	Expression
nfop	|- F/_ x <. A , B >.

Proof of Theorem nfop

Step	Hyp	Ref	Expression
1		dfopif 4399	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		nfop.1	. . . . 5 |- F/_ x A
3	2	nfel1 2779	. . . 4 |- F/ x A e. _V
4		nfop.2	. . . . 5 |- F/_ x B
5	4	nfel1 2779	. . . 4 |- F/ x B e. _V
6	3, 5	nfan 1828	. . 3 |- F/ x ( A e. _V /\ B e. _V )
7	2	nfsn 4242	. . . 4 |- F/_ x { A }
8	2, 4	nfpr 4232	. . . 4 |- F/_ x { A , B }
9	7, 8	nfpr 4232	. . 3 |- F/_ x { { A } , { A , B } }
10		nfcv 2764	. . 3 |- F/_ x (/)
11	6, 9, 10	nfif 4115	. 2 |- F/_ x if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
12	1, 11	nfcxfr 2762	1 |- F/_ x <. A , B >.

Syntax hints:   /\ wa 384   e. wcel 1990   F/_wnfc 2751   _Vcvv 3200   (/)c0 3915   ifcif 4086   {csn 4177   {cpr 4179   <.cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  nfopd  4419  moop2  4966  iunopeqop  4981  fliftfuns  6564  dfmpt2  7267  qliftfuns  7834  xpf1o  8122  nfseq  12811  txcnp  21423  cnmpt1t  21468  cnmpt2t  21476  flfcnp2  21811  bnj958  31010  bnj1000  31011  bnj1446  31113  bnj1447  31114  bnj1448  31115  bnj1466  31121  bnj1467  31122  bnj1519  31133  bnj1520  31134  bnj1529  31138  nosupbnd2  31862  poimirlem26  33435  nfopdALT  34258  nfaov  41259