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

Theorem rexbiia 3250
Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
rexbiia.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rexbiia (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)

Proof of Theorem rexbiia
StepHypRef Expression
1 rexbiia.1 . . 3 (𝑥𝐴 → (𝜑𝜓))
21pm5.32i 575 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3249 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wcel 2106  wrex 3143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-rex 3148
This theorem is referenced by:  rexanid  3256  2rexbiia  3302  ceqsrexbv  3653  reu8  3727  f1oweALT  7667  reldm  7737  seqomlem2  8081  fofinf1o  8791  wdom2d  9036  unbndrank  9263  cfsmolem  9684  fin1a2lem5  9818  fin1a2lem6  9819  infm3  11592  wwlktovfo  14315  even2n  15683  cycsubmel  18275  znf1o  20614  lmres  21824  ist1-2  21871  itg2monolem1  24266  lhop1lem  24525  elaa  24820  ulmcau  24898  reeff1o  24950  recosf1o  25032  chpo1ubb  25971  istrkg2ld  26160  wlkswwlksf1o  27572  wwlksnextsurj  27593  nmopnegi  29657  nmop0  29678  nmfn0  29679  adjbd1o  29777  atom1d  30045  abfmpunirn  30313  rearchi  30830  eulerpartgbij  31517  eulerpartlemgh  31523  subfacp1lem3  32314  dfrdg2  32925  heiborlem7  34964  qsresid  35451  eq0rabdioph  39235  elicores  41671  liminfpnfuz  41959  xlimpnfxnegmnf2  42001  fourierdlem70  42324  fourierdlem80  42334  ovolval3  42792  rexrsb  43161
  Copyright terms: Public domain W3C validator