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

Theorem nfop 3812
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 3793 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 nfop.1 . . . . 5  |-  F/_ x A
32nfel1 2429 . . . 4  |-  F/ x  A  e.  _V
4 nfop.2 . . . . 5  |-  F/_ x B
54nfel1 2429 . . . 4  |-  F/ x  B  e.  _V
63, 5nfan 1771 . . 3  |-  F/ x
( A  e.  _V  /\  B  e.  _V )
72nfsn 3691 . . . 4  |-  F/_ x { A }
82, 4nfpr 3680 . . . 4  |-  F/_ x { A ,  B }
97, 8nfpr 3680 . . 3  |-  F/_ x { { A } ,  { A ,  B } }
10 nfcv 2419 . . 3  |-  F/_ x (/)
116, 9, 10nfif 3589 . 2  |-  F/_ x if ( ( A  e. 
_V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
121, 11nfcxfr 2416 1  |-  F/_ x <. A ,  B >.
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1684   F/_wnfc 2406   _Vcvv 2788   (/)c0 3455   ifcif 3565   {csn 3640   {cpr 3641   <.cop 3643
This theorem is referenced by:  nfopd  3813  moop2  4261  fliftfuns  5813  dfmpt2  6209  qliftfuns  6745  xpf1o  7023  nfseq  11056  txcnp  17314  cnmpt1t  17359  cnmpt2t  17367  flfcnp2  17702  sbcopg  24022  nfaov  28039  bnj958  28972  bnj1000  28973  bnj1446  29075  bnj1447  29076  bnj1448  29077  bnj1466  29083  bnj1467  29084  bnj1519  29095  bnj1520  29096  bnj1529  29100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649
  Copyright terms: Public domain W3C validator