Theorem rexbiia 3069

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

Syntax hints:   → wi 4   ↔ wb 196   ∈ wcel 2030  ∃wrex 2942

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-rex 2947

This theorem is referenced by:  2rexbiia  3084  ceqsrexbv  3368  reu8  3435  f1oweALT  7194  reldm  7263  seqomlem2  7591  fofinf1o  8282  wdom2d  8526  unbndrank  8743  cfsmolem  9130  fin1a2lem5  9264  fin1a2lem6  9265  infm3  11020  wwlktovfo  13747  even2n  15113  znf1o  19948  lmres  21152  ist1-2  21199  itg2monolem1  23562  lhop1lem  23821  elaa  24116  ulmcau  24194  reeff1o  24246  recosf1o  24326  chpo1ubb  25215  istrkg2ld  25404  wlkpwwlkf1ouspgr  26833  wlknwwlksnsur  26844  wlkwwlksur  26851  wwlksnextsur  26863  nmopnegi  28952  nmop0  28973  nmfn0  28974  adjbd1o  29072  atom1d  29340  abfmpunirn  29580  rearchi  29970  eulerpartgbij  30562  eulerpartlemgh  30568  subfacp1lem3  31290  dfrdg2  31825  heiborlem7  33746  qsresid  34237  eq0rabdioph  37657  elicores  40078  fourierdlem70  40711  fourierdlem80  40721  ovolval3  41182  rexrsb  41490