Theorem rexbiia 3116

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2149  ∃wrex 3095

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  rexbii  3118  rexanid  3120  2rexbiia  3232  ceqsrexbv  3624  reu8  3705  f1oweALT  7965  reldm  8037  seqomlem2  8434  fofinf1o  9285  wdom2d  9538  unbndrank  9810  cfsmolem  10250  fin1a2lem5  10384  fin1a2lem6  10385  infm3  12170  wwlktovfo  14991  even2n  16396  smndex1mnd  18968  cycsubmel  19267  znf1o  21666  lmres  23422  ist1-2  23469  itg2monolem1  25874  lhop1lem  26137  elaa  26442  ulmcau  26520  reeff1o  26572  recosf1o  26662  chpo1ubb  27607  noetainflem4  27866  bdayn0sf1o  28525  istrkg2ld  28691  wlkswwlksf1o  30165  wwlksnextsurj  30186  nmopnegi  32254  nmop0  32275  nmfn0  32276  adjbd1o  32374  atom1d  32642  abfmpunirn  32934  rearchi  33605  eulerpartgbij  34703  eulerpartlemgh  34709  noinfepregs  35465  subfacp1lem3  35569  dfrdg2  36180  heiborlem7  38351  qsresid  38865  cxpi11d  42987  fimgmcyc  43187  eq0rabdioph  43392  elicores  46134  liminfpnfuz  46415  xlimpnfxnegmnf2  46457  fourierdlem70  46775  fourierdlem80  46785  ovolval3  47246  rexrsb  47719  slotresfo  49555  basresposfo  49634