ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rspc2ev Unicode version

Theorem rspc2ev 2778
Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
Hypotheses
Ref Expression
rspc2v.1  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
rspc2v.2  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
Assertion
Ref Expression
rspc2ev  |-  ( ( A  e.  C  /\  B  e.  D  /\  ps )  ->  E. x  e.  C  E. y  e.  D  ph )
Distinct variable groups:    x, y, A   
y, B    x, C    x, D, y    ch, x    ps, y
Allowed substitution hints:    ph( x, y)    ps( x)    ch( y)    B( x)    C( y)

Proof of Theorem rspc2ev
StepHypRef Expression
1 rspc2v.2 . . . . 5  |-  ( y  =  B  ->  ( ch 
<->  ps ) )
21rspcev 2763 . . . 4  |-  ( ( B  e.  D  /\  ps )  ->  E. y  e.  D  ch )
32anim2i 339 . . 3  |-  ( ( A  e.  C  /\  ( B  e.  D  /\  ps ) )  -> 
( A  e.  C  /\  E. y  e.  D  ch ) )
433impb 1162 . 2  |-  ( ( A  e.  C  /\  B  e.  D  /\  ps )  ->  ( A  e.  C  /\  E. y  e.  D  ch ) )
5 rspc2v.1 . . . 4  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
65rexbidv 2415 . . 3  |-  ( x  =  A  ->  ( E. y  e.  D  ph  <->  E. y  e.  D  ch ) )
76rspcev 2763 . 2  |-  ( ( A  e.  C  /\  E. y  e.  D  ch )  ->  E. x  e.  C  E. y  e.  D  ph )
84, 7syl 14 1  |-  ( ( A  e.  C  /\  B  e.  D  /\  ps )  ->  E. x  e.  C  E. y  e.  D  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    /\ w3a 947    = wceq 1316    e. wcel 1465   E.wrex 2394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662
This theorem is referenced by:  rspc3ev  2780  opelxp  4539  rspceov  5781  2dom  6667  apreim  8333  addcn2  11047  mulcn2  11049  divalglemnn  11542  bezoutlema  11614  bezoutlemb  11615  txuni2  12352  txopn  12361  txdis  12373  txdis1cn  12374  xmettxlem  12605
  Copyright terms: Public domain W3C validator