Theorem rexbiia 3116

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 584	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rexbii2 3114	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2149  ∃wrex 3095

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  rexbii  3118  rexanid  3120  2rexbiia  3232  ceqsrexbv  3624  reu8  3705  f1oweALT  7969  reldm  8041  seqomlem2  8438  fofinf1o  9289  wdom2d  9542  unbndrank  9814  cfsmolem  10254  fin1a2lem5  10388  fin1a2lem6  10389  infm3  12174  wwlktovfo  14995  even2n  16400  smndex1mnd  18972  cycsubmel  19271  znf1o  21670  lmres  23426  ist1-2  23473  itg2monolem1  25878  lhop1lem  26141  elaa  26446  ulmcau  26524  reeff1o  26576  recosf1o  26666  chpo1ubb  27611  noetainflem4  27870  bdayn0sf1o  28529  istrkg2ld  28695  wlkswwlksf1o  30169  wwlksnextsurj  30190  nmopnegi  32258  nmop0  32279  nmfn0  32280  adjbd1o  32378  atom1d  32646  abfmpunirn  32938  rearchi  33609  eulerpartgbij  34707  eulerpartlemgh  34713  noinfepregs  35479  subfacp1lem3  35607  dfrdg2  36218  heiborlem7  38390  qsresid  38904  cxpi11d  43028  fimgmcyc  43228  eq0rabdioph  43433  elicores  46175  liminfpnfuz  46456  xlimpnfxnegmnf2  46498  fourierdlem70  46816  fourierdlem80  46826  ovolval3  47287  rexrsb  47760  slotresfo  49596  basresposfo  49675