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

Theorem r2exlem 2909
Description: Lemma factoring out common proof steps in r2exf 2910 an r2ex 2912. 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 1698 . . 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 313 . 2  |-  ( E. x  -.  A. y
( ( x  e.  A  /\  y  e.  B )  ->  -.  ph )  <->  -.  A. x  e.  A  A. y  e.  B  -.  ph )
4 alinexa 1712 . . . 4  |-  ( A. y ( ( x  e.  A  /\  y  e.  B )  ->  -.  ph )  <->  -.  E. y
( ( x  e.  A  /\  y  e.  B )  /\  ph ) )
54con2bii 334 . . 3  |-  ( E. y ( ( x  e.  A  /\  y  e.  B )  /\  ph ) 
<->  -.  A. y ( ( x  e.  A  /\  y  e.  B
)  ->  -.  ph )
)
65exbii 1717 . 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 2833 . . . . 5  |-  ( A. y  e.  B  -.  ph  <->  -. 
E. y  e.  B  ph )
87ralbii 2818 . . . 4  |-  ( A. x  e.  A  A. y  e.  B  -.  ph  <->  A. x  e.  A  -.  E. y  e.  B  ph )
9 ralnex 2833 . . . 4  |-  ( A. x  e.  A  -.  E. y  e.  B  ph  <->  -. 
E. x  e.  A  E. y  e.  B  ph )
108, 9bitri 253 . . 3  |-  ( A. x  e.  A  A. y  e.  B  -.  ph  <->  -. 
E. x  e.  A  E. y  e.  B  ph )
1110con2bii 334 . 2  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  -.  A. x  e.  A  A. y  e.  B  -.  ph )
123, 6, 113bitr4ri 282 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 188    /\ wa 371   A.wal 1441   E.wex 1662    e. wcel 1886   A.wral 2736   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-ral 2741  df-rex 2742
This theorem is referenced by:  r2exf  2910  r2ex  2912
  Copyright terms: Public domain W3C validator