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

Theorem nfop 3992
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
StepHypRef Expression
1 dfopif 3973 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 nfop.1 . . . . 5  |-  F/_ x A
32nfel1 2581 . . . 4  |-  F/ x  A  e.  _V
4 nfop.2 . . . . 5  |-  F/_ x B
54nfel1 2581 . . . 4  |-  F/ x  B  e.  _V
63, 5nfan 1846 . . 3  |-  F/ x
( A  e.  _V  /\  B  e.  _V )
72nfsn 3858 . . . 4  |-  F/_ x { A }
82, 4nfpr 3847 . . . 4  |-  F/_ x { A ,  B }
97, 8nfpr 3847 . . 3  |-  F/_ x { { A } ,  { A ,  B } }
10 nfcv 2571 . . 3  |-  F/_ x (/)
116, 9, 10nfif 3755 . 2  |-  F/_ x if ( ( A  e. 
_V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
121, 11nfcxfr 2568 1  |-  F/_ x <. A ,  B >.
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1725   F/_wnfc 2558   _Vcvv 2948   (/)c0 3620   ifcif 3731   {csn 3806   {cpr 3807   <.cop 3809
This theorem is referenced by:  nfopd  3993  moop2  4443  fliftfuns  6027  dfmpt2  6428  qliftfuns  6982  xpf1o  7260  nfseq  11321  txcnp  17640  cnmpt1t  17685  cnmpt2t  17693  flfcnp2  18027  sbcopg  25114  nfaov  27957  bnj958  29165  bnj1000  29166  bnj1446  29268  bnj1447  29269  bnj1448  29270  bnj1466  29276  bnj1467  29277  bnj1519  29288  bnj1520  29289  bnj1529  29293
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815
  Copyright terms: Public domain W3C validator