Theorem rexbiia 3093

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexbii  3095  rexanid  3097  2rexbiia  3216  ceqsrexbv  3643  reu8  3728  f1oweALT  7954  reldm  8025  seqomlem2  8446  fofinf1o  9323  wdom2d  9571  unbndrank  9833  cfsmolem  10261  fin1a2lem5  10395  fin1a2lem6  10396  infm3  12169  wwlktovfo  14905  even2n  16281  smndex1mnd  18787  cycsubmel  19071  znf1o  21091  lmres  22786  ist1-2  22833  itg2monolem1  25250  lhop1lem  25512  elaa  25811  ulmcau  25889  reeff1o  25941  recosf1o  26026  chpo1ubb  26964  noetainflem4  27223  istrkg2ld  27691  wlkswwlksf1o  29113  wwlksnextsurj  29134  nmopnegi  31196  nmop0  31217  nmfn0  31218  adjbd1o  31316  atom1d  31584  abfmpunirn  31855  rearchi  32430  eulerpartgbij  33309  eulerpartlemgh  33315  subfacp1lem3  34111  dfrdg2  34705  heiborlem7  36623  qsresid  37132  eq0rabdioph  41447  elicores  44181  liminfpnfuz  44467  xlimpnfxnegmnf2  44509  fourierdlem70  44827  fourierdlem80  44837  ovolval3  45298  rexrsb  45743