Theorem rexbiia 3022

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

Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977  ∃wrex 2897

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902

This theorem is referenced by:  2rexbiia  3037  ceqsrexbv  3307  reu8  3369  f1oweALT  7043  reldm  7110  seqomlem2  7433  fofinf1o  8126  wdom2d  8368  unbndrank  8588  cfsmolem  8975  fin1a2lem5  9109  fin1a2lem6  9110  infm3  10861  wwlktovfo  13549  even2n  14904  znf1o  19719  lmres  20914  ist1-2  20961  itg2monolem1  23323  lhop1lem  23580  elaa  23875  ulmcau  23953  reeff1o  24005  recosf1o  24085  chpo1ubb  24970  istrkg2ld  25159  wlknwwlknsur  26240  wlkiswwlksur  26247  wwlkextsur  26259  nmopnegi  28208  nmop0  28229  nmfn0  28230  adjbd1o  28328  atom1d  28596  abfmpunirn  28832  rearchi  29173  eulerpartgbij  29761  eulerpartlemgh  29767  subfacp1lem3  30418  dfrdg2  30945  heiborlem7  32786  eq0rabdioph  36358  elicores  38607  fourierdlem70  39069  fourierdlem80  39079  ovolval3  39537  rexrsb  39818  1wlkpwwlkf1ouspgr  41076  wlknwwlksnsur  41087  wlkwwlksur  41094  wwlksnextsur  41106