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

Theorem r2exlem 2946
Description: Lemma factoring out common proof steps in r2exf 2947 an r2ex 2949. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020.)
Hypothesis
Ref Expression
r2exlem.1  |-  ( A. x  e.  A  A. y  e.  B  -.  ph  <->  A. x A. y ( ( x  e.  A  /\  y  e.  B
)  ->  -.  ph )
)
Assertion
Ref Expression
r2exlem  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x E. y ( ( x  e.  A  /\  y  e.  B )  /\  ph ) )

Proof of Theorem r2exlem
StepHypRef Expression
1 exnal 1695 . . 3  |-  ( E. x  -.  A. y
( ( x  e.  A  /\  y  e.  B )  ->  -.  ph )  <->  -.  A. x A. y ( ( x  e.  A  /\  y  e.  B )  ->  -.  ph ) )
2 r2exlem.1 . . 3  |-  ( A. x  e.  A  A. y  e.  B  -.  ph  <->  A. x A. y ( ( x  e.  A  /\  y  e.  B
)  ->  -.  ph )
)
31, 2xchbinxr 312 . 2  |-  ( E. x  -.  A. y
( ( x  e.  A  /\  y  e.  B )  ->  -.  ph )  <->  -.  A. x  e.  A  A. y  e.  B  -.  ph )
4 alinexa 1708 . . . 4  |-  ( A. y ( ( x  e.  A  /\  y  e.  B )  ->  -.  ph )  <->  -.  E. y
( ( x  e.  A  /\  y  e.  B )  /\  ph ) )
54con2bii 333 . . 3  |-  ( E. y ( ( x  e.  A  /\  y  e.  B )  /\  ph ) 
<->  -.  A. y ( ( x  e.  A  /\  y  e.  B
)  ->  -.  ph )
)
65exbii 1712 . 2  |-  ( E. x E. y ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  <->  E. x  -.  A. y ( ( x  e.  A  /\  y  e.  B )  ->  -.  ph ) )
7 ralnex 2869 . . . . 5  |-  ( A. y  e.  B  -.  ph  <->  -. 
E. y  e.  B  ph )
87ralbii 2854 . . . 4  |-  ( A. x  e.  A  A. y  e.  B  -.  ph  <->  A. x  e.  A  -.  E. y  e.  B  ph )
9 ralnex 2869 . . . 4  |-  ( A. x  e.  A  -.  E. y  e.  B  ph  <->  -. 
E. x  e.  A  E. y  e.  B  ph )
108, 9bitri 252 . . 3  |-  ( A. x  e.  A  A. y  e.  B  -.  ph  <->  -. 
E. x  e.  A  E. y  e.  B  ph )
1110con2bii 333 . 2  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  -.  A. x  e.  A  A. y  e.  B  -.  ph )
123, 6, 113bitr4ri 281 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x E. y ( ( x  e.  A  /\  y  e.  B )  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435   E.wex 1659    e. wcel 1867   A.wral 2773   E.wrex 2774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2778  df-rex 2779
This theorem is referenced by:  r2exf  2947  r2ex  2949
  Copyright terms: Public domain W3C validator