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

Theorem nfop 4094
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 4075 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 nfop.1 . . . . 5  |-  F/_ x A
32nfel1 2604 . . . 4  |-  F/ x  A  e.  _V
4 nfop.2 . . . . 5  |-  F/_ x B
54nfel1 2604 . . . 4  |-  F/ x  B  e.  _V
63, 5nfan 1861 . . 3  |-  F/ x
( A  e.  _V  /\  B  e.  _V )
72nfsn 3953 . . . 4  |-  F/_ x { A }
82, 4nfpr 3942 . . . 4  |-  F/_ x { A ,  B }
97, 8nfpr 3942 . . 3  |-  F/_ x { { A } ,  { A ,  B } }
10 nfcv 2589 . . 3  |-  F/_ x (/)
116, 9, 10nfif 3837 . 2  |-  F/_ x if ( ( A  e. 
_V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
121, 11nfcxfr 2587 1  |-  F/_ x <. A ,  B >.
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1756   F/_wnfc 2575   _Vcvv 2991   (/)c0 3656   ifcif 3810   {csn 3896   {cpr 3898   <.cop 3902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2993  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903
This theorem is referenced by:  nfopd  4095  csbopg  4096  moop2  4605  fliftfuns  6026  dfmpt2  6682  qliftfuns  7206  xpf1o  7492  nfseq  11835  txcnp  19212  cnmpt1t  19257  cnmpt2t  19265  flfcnp2  19599  nfaov  30108  bnj958  31956  bnj1000  31957  bnj1446  32059  bnj1447  32060  bnj1448  32061  bnj1466  32067  bnj1467  32068  bnj1519  32079  bnj1520  32080  bnj1529  32084
  Copyright terms: Public domain W3C validator