Theorem rexbiia 3089

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2098  ∃wrex 3067

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3068

This theorem is referenced by:  rexbii  3091  rexanid  3093  2rexbiia  3213  ceqsrexbv  3644  reu8  3730  f1oweALT  7982  reldm  8054  seqomlem2  8478  fofinf1o  9359  wdom2d  9611  unbndrank  9873  cfsmolem  10301  fin1a2lem5  10435  fin1a2lem6  10436  infm3  12211  wwlktovfo  14949  even2n  16326  smndex1mnd  18869  cycsubmel  19162  znf1o  21492  lmres  23224  ist1-2  23271  itg2monolem1  25700  lhop1lem  25966  elaa  26271  ulmcau  26351  reeff1o  26404  recosf1o  26489  chpo1ubb  27434  noetainflem4  27693  0reno  28245  istrkg2ld  28284  wlkswwlksf1o  29710  wwlksnextsurj  29731  nmopnegi  31795  nmop0  31816  nmfn0  31817  adjbd1o  31915  atom1d  32183  abfmpunirn  32459  rearchi  33082  eulerpartgbij  34025  eulerpartlemgh  34031  subfacp1lem3  34825  dfrdg2  35424  heiborlem7  37323  qsresid  37829  cxpi11d  41945  eq0rabdioph  42227  elicores  44947  liminfpnfuz  45233  xlimpnfxnegmnf2  45275  fourierdlem70  45593  fourierdlem80  45603  ovolval3  46064  rexrsb  46509