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

Theorem eubii 1986
Description: Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
Hypothesis
Ref Expression
eubii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
eubii  |-  ( E! x ph  <->  E! x ps )

Proof of Theorem eubii
StepHypRef Expression
1 eubii.1 . . . 4  |-  ( ph  <->  ps )
21a1i 9 . . 3  |-  ( T. 
->  ( ph  <->  ps )
)
32eubidv 1985 . 2  |-  ( T. 
->  ( E! x ph  <->  E! x ps ) )
43mptru 1325 1  |-  ( E! x ph  <->  E! x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   T. wtru 1317   E!weu 1977
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-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-eu 1980
This theorem is referenced by:  cbveu  2001  2eu7  2071  reubiia  2592  cbvreu  2629  reuv  2679  euxfr2dc  2842  euxfrdc  2843  2reuswapdc  2861  reuun2  3329  zfnuleu  4022  copsexg  4136  funeu2  5119  funcnv3  5155  fneu2  5198  tz6.12  5417  f1ompt  5539  fsn  5560  climreu  11034  divalgb  11549  txcn  12371
  Copyright terms: Public domain W3C validator