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  3599  reu8  3680  f1oweALT  7918  reldm  7990  seqomlem2  8383  fofinf1o  9235  wdom2d  9488  unbndrank  9757  cfsmolem  10183  fin1a2lem5  10317  fin1a2lem6  10318  infm3  12106  wwlktovfo  14911  even2n  16302  smndex1mnd  18872  cycsubmel  19166  znf1o  21541  lmres  23275  ist1-2  23322  itg2monolem1  25727  lhop1lem  25990  elaa  26293  ulmcau  26373  reeff1o  26425  recosf1o  26512  chpo1ubb  27458  noetainflem4  27718  bdayn0sf1o  28376  istrkg2ld  28542  wlkswwlksf1o  29962  wwlksnextsurj  29983  nmopnegi  32051  nmop0  32072  nmfn0  32073  adjbd1o  32171  atom1d  32439  abfmpunirn  32740  rearchi  33421  eulerpartgbij  34532  eulerpartlemgh  34538  noinfepregs  35293  subfacp1lem3  35380  dfrdg2  35991  heiborlem7  38152  qsresid  38666  cxpi11d  42789  fimgmcyc  42993  eq0rabdioph  43222  elicores  45981  liminfpnfuz  46262  xlimpnfxnegmnf2  46304  fourierdlem70  46622  fourierdlem80  46632  ovolval3  47093  rexrsb  47560  slotresfo  49386  basresposfo  49465