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

Theorem nfop 4219
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 4200 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 nfop.1 . . . . 5  |-  F/_ x A
32nfel1 2632 . . . 4  |-  F/ x  A  e.  _V
4 nfop.2 . . . . 5  |-  F/_ x B
54nfel1 2632 . . . 4  |-  F/ x  B  e.  _V
63, 5nfan 1933 . . 3  |-  F/ x
( A  e.  _V  /\  B  e.  _V )
72nfsn 4073 . . . 4  |-  F/_ x { A }
82, 4nfpr 4063 . . . 4  |-  F/_ x { A ,  B }
97, 8nfpr 4063 . . 3  |-  F/_ x { { A } ,  { A ,  B } }
10 nfcv 2616 . . 3  |-  F/_ x (/)
116, 9, 10nfif 3958 . 2  |-  F/_ x if ( ( A  e. 
_V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
121, 11nfcxfr 2614 1  |-  F/_ x <. A ,  B >.
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367    e. wcel 1823   F/_wnfc 2602   _Vcvv 3106   (/)c0 3783   ifcif 3929   {csn 4016   {cpr 4018   <.cop 4022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023
This theorem is referenced by:  nfopd  4220  csbopg  4221  moop2  4731  fliftfuns  6187  dfmpt2  6863  qliftfuns  7390  xpf1o  7672  nfseq  12099  txcnp  20287  cnmpt1t  20332  cnmpt2t  20340  flfcnp2  20674  nfaov  32503  bnj958  34399  bnj1000  34400  bnj1446  34502  bnj1447  34503  bnj1448  34504  bnj1466  34510  bnj1467  34511  bnj1519  34522  bnj1520  34523  bnj1529  34527
  Copyright terms: Public domain W3C validator