Theorem rexbiia 3083

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexbii  3085  rexanid  3087  2rexbiia  3199  ceqsrexbv  3612  reu8  3693  f1oweALT  7926  reldm  7998  seqomlem2  8392  fofinf1o  9244  wdom2d  9497  unbndrank  9766  cfsmolem  10192  fin1a2lem5  10326  fin1a2lem6  10327  infm3  12113  wwlktovfo  14893  even2n  16281  smndex1mnd  18847  cycsubmel  19141  znf1o  21518  lmres  23256  ist1-2  23303  itg2monolem1  25719  lhop1lem  25986  elaa  26292  ulmcau  26372  reeff1o  26425  recosf1o  26512  chpo1ubb  27460  noetainflem4  27720  bdayn0sf1o  28378  istrkg2ld  28544  wlkswwlksf1o  29964  wwlksnextsurj  29985  nmopnegi  32052  nmop0  32073  nmfn0  32074  adjbd1o  32172  atom1d  32440  abfmpunirn  32741  rearchi  33438  eulerpartgbij  34549  eulerpartlemgh  34555  noinfepregs  35308  subfacp1lem3  35395  dfrdg2  36006  heiborlem7  38065  qsresid  38579  cxpi11d  42710  fimgmcyc  42901  eq0rabdioph  43130  elicores  45890  liminfpnfuz  46171  xlimpnfxnegmnf2  46213  fourierdlem70  46531  fourierdlem80  46541  ovolval3  47002  rexrsb  47457  slotresfo  49255  basresposfo  49334