Theorem rexbiia 3092

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

Step	Hyp	Ref	Expression
1		rexbiia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
2	1	pm5.32i 574	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rexbii2 3090	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  rexbii  3094  rexanid  3096  2rexbiia  3218  ceqsrexbv  3656  reu8  3739  f1oweALT  7997  reldm  8069  seqomlem2  8491  fofinf1o  9372  wdom2d  9620  unbndrank  9882  cfsmolem  10310  fin1a2lem5  10444  fin1a2lem6  10445  infm3  12227  wwlktovfo  14997  even2n  16379  smndex1mnd  18923  cycsubmel  19218  znf1o  21570  lmres  23308  ist1-2  23355  itg2monolem1  25785  lhop1lem  26052  elaa  26358  ulmcau  26438  reeff1o  26491  recosf1o  26577  chpo1ubb  27525  noetainflem4  27785  0reno  28429  istrkg2ld  28468  wlkswwlksf1o  29899  wwlksnextsurj  29920  nmopnegi  31984  nmop0  32005  nmfn0  32006  adjbd1o  32104  atom1d  32372  abfmpunirn  32662  rearchi  33374  eulerpartgbij  34374  eulerpartlemgh  34380  subfacp1lem3  35187  dfrdg2  35796  heiborlem7  37824  qsresid  38326  cxpi11d  42379  fimgmcyc  42544  eq0rabdioph  42787  elicores  45546  liminfpnfuz  45831  xlimpnfxnegmnf2  45873  fourierdlem70  46191  fourierdlem80  46201  ovolval3  46662  rexrsb  47112