Theorem rexbiia 3092

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  ∃wrex 3070

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 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  rexbii  3094  rexanid  3096  2rexbiia  3215  ceqsrexbv  3644  reu8  3729  f1oweALT  7958  reldm  8029  seqomlem2  8450  fofinf1o  9326  wdom2d  9574  unbndrank  9836  cfsmolem  10264  fin1a2lem5  10398  fin1a2lem6  10399  infm3  12172  wwlktovfo  14908  even2n  16284  smndex1mnd  18790  cycsubmel  19076  znf1o  21106  lmres  22803  ist1-2  22850  itg2monolem1  25267  lhop1lem  25529  elaa  25828  ulmcau  25906  reeff1o  25958  recosf1o  26043  chpo1ubb  26981  noetainflem4  27240  istrkg2ld  27708  wlkswwlksf1o  29130  wwlksnextsurj  29151  nmopnegi  31213  nmop0  31234  nmfn0  31235  adjbd1o  31333  atom1d  31601  abfmpunirn  31872  rearchi  32456  eulerpartgbij  33366  eulerpartlemgh  33372  subfacp1lem3  34168  dfrdg2  34762  heiborlem7  36680  qsresid  37189  eq0rabdioph  41504  elicores  44236  liminfpnfuz  44522  xlimpnfxnegmnf2  44564  fourierdlem70  44882  fourierdlem80  44892  ovolval3  45353  rexrsb  45798