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

Theorem nfop 3936
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 3917 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 nfop.1 . . . . 5  |-  F/_ x A
32nfel1 2527 . . . 4  |-  F/ x  A  e.  _V
4 nfop.2 . . . . 5  |-  F/_ x B
54nfel1 2527 . . . 4  |-  F/ x  B  e.  _V
63, 5nfan 1836 . . 3  |-  F/ x
( A  e.  _V  /\  B  e.  _V )
72nfsn 3803 . . . 4  |-  F/_ x { A }
82, 4nfpr 3792 . . . 4  |-  F/_ x { A ,  B }
97, 8nfpr 3792 . . 3  |-  F/_ x { { A } ,  { A ,  B } }
10 nfcv 2517 . . 3  |-  F/_ x (/)
116, 9, 10nfif 3700 . 2  |-  F/_ x if ( ( A  e. 
_V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
121, 11nfcxfr 2514 1  |-  F/_ x <. A ,  B >.
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1717   F/_wnfc 2504   _Vcvv 2893   (/)c0 3565   ifcif 3676   {csn 3751   {cpr 3752   <.cop 3754
This theorem is referenced by:  nfopd  3937  moop2  4386  fliftfuns  5969  dfmpt2  6370  qliftfuns  6921  xpf1o  7199  nfseq  11254  txcnp  17567  cnmpt1t  17612  cnmpt2t  17620  flfcnp2  17954  sbcopg  24899  nfaov  27706  bnj958  28643  bnj1000  28644  bnj1446  28746  bnj1447  28747  bnj1448  28748  bnj1466  28754  bnj1467  28755  bnj1519  28766  bnj1520  28767  bnj1529  28771
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-v 2895  df-dif 3260  df-un 3262  df-in 3264  df-ss 3271  df-nul 3566  df-if 3677  df-sn 3757  df-pr 3758  df-op 3760
  Copyright terms: Public domain W3C validator