Theorem rexbiia 3082

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 3080	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∃wrex 3061

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 3062

This theorem is referenced by:  rexbii  3084  rexanid  3086  2rexbiia  3198  ceqsrexbv  3598  reu8  3679  f1oweALT  7925  reldm  7997  seqomlem2  8390  fofinf1o  9242  wdom2d  9495  unbndrank  9766  cfsmolem  10192  fin1a2lem5  10326  fin1a2lem6  10327  infm3  12115  wwlktovfo  14920  even2n  16311  smndex1mnd  18881  cycsubmel  19175  znf1o  21531  lmres  23265  ist1-2  23312  itg2monolem1  25717  lhop1lem  25980  elaa  26282  ulmcau  26360  reeff1o  26412  recosf1o  26499  chpo1ubb  27444  noetainflem4  27704  bdayn0sf1o  28362  istrkg2ld  28528  wlkswwlksf1o  29947  wwlksnextsurj  29968  nmopnegi  32036  nmop0  32057  nmfn0  32058  adjbd1o  32156  atom1d  32424  abfmpunirn  32725  rearchi  33406  eulerpartgbij  34516  eulerpartlemgh  34522  noinfepregs  35277  subfacp1lem3  35364  dfrdg2  35975  heiborlem7  38138  qsresid  38652  cxpi11d  42775  fimgmcyc  42979  eq0rabdioph  43208  elicores  45963  liminfpnfuz  46244  xlimpnfxnegmnf2  46286  fourierdlem70  46604  fourierdlem80  46614  ovolval3  47075  rexrsb  47548  slotresfo  49374  basresposfo  49453