Theorem rexbiia 3107

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3087

This theorem is used by:  rexbii  3109  rexanid  3111  2rexbiia  3223  ceqsrexbv  3610  reu8  3691  f1oweALT  7969  reldm  8041  seqomlem2  8440  fofinf1o  9299  wdom2d  9552  unbndrank  9824  cfsmolem  10272  fin1a2lem5  10406  fin1a2lem6  10407  infm3  12198  wwlktovfo  15031  even2n  16432  smndex1mnd  19022  cycsubmel  19328  znf1o  21764  lmres  23525  ist1-2  23572  itg2monolem1  25978  lhop1lem  26240  elaa  26548  ulmcau  26631  reeff1o  26683  recosf1o  26772  chpo1ubb  27717  noetainflem4  27976  bdayn0sf1o  28635  istrkg2ld  28801  wlkswwlksf1o  30347  wwlksnextsurj  30368  nmopnegi  32446  nmop0  32467  nmfn0  32468  adjbd1o  32566  atom1d  32834  abfmpunirn  33125  rearchi  33786  eulerpartgbij  34883  eulerpartlemgh  34889  noinfepregs  35659  subfacp1lem3  35761  dfrdg2  36372  heiborlem7  38567  qsresid  39079  cxpi11d  43218  fimgmcyc  43416  eq0rabdioph  43621  elicores  46363  liminfpnfuz  46644  xlimpnfxnegmnf2  46686  fourierdlem70  47004  fourierdlem80  47014  ovolval3  47475  rexrsb  47988  slotresfo  49825  basresposfo  49904