Theorem rexbiia 3082

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 3080	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∃wrex 3061

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 3062

This theorem is referenced by:  rexbii  3084  rexanid  3086  2rexbiia  3206  ceqsrexbv  3640  reu8  3721  f1oweALT  7976  reldm  8048  seqomlem2  8470  fofinf1o  9349  wdom2d  9599  unbndrank  9861  cfsmolem  10289  fin1a2lem5  10423  fin1a2lem6  10424  infm3  12206  wwlktovfo  14982  even2n  16366  smndex1mnd  18893  cycsubmel  19188  znf1o  21517  lmres  23243  ist1-2  23290  itg2monolem1  25708  lhop1lem  25975  elaa  26281  ulmcau  26361  reeff1o  26414  recosf1o  26501  chpo1ubb  27449  noetainflem4  27709  bdayn0sf1o  28316  0reno  28405  istrkg2ld  28444  wlkswwlksf1o  29866  wwlksnextsurj  29887  nmopnegi  31951  nmop0  31972  nmfn0  31973  adjbd1o  32071  atom1d  32339  abfmpunirn  32635  rearchi  33366  eulerpartgbij  34409  eulerpartlemgh  34415  subfacp1lem3  35209  dfrdg2  35818  heiborlem7  37846  qsresid  38348  cxpi11d  42359  fimgmcyc  42524  eq0rabdioph  42766  elicores  45529  liminfpnfuz  45812  xlimpnfxnegmnf2  45854  fourierdlem70  46172  fourierdlem80  46182  ovolval3  46643  rexrsb  47096  slotresfo  48840  basresposfo  48919