Theorem rexbiia 3106

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2141  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexbii  3108  rexanid  3110  2rexbiia  3222  ceqsrexbv  3614  reu8  3694  f1oweALT  7948  reldm  8020  seqomlem2  8416  fofinf1o  9269  wdom2d  9522  unbndrank  9794  cfsmolem  10221  fin1a2lem5  10355  fin1a2lem6  10356  infm3  12145  wwlktovfo  14965  even2n  16367  smndex1mnd  18938  cycsubmel  19232  znf1o  21591  lmres  23348  ist1-2  23395  itg2monolem1  25800  lhop1lem  26063  elaa  26368  ulmcau  26446  reeff1o  26498  recosf1o  26588  chpo1ubb  27533  noetainflem4  27792  bdayn0sf1o  28451  istrkg2ld  28617  wlkswwlksf1o  30036  wwlksnextsurj  30057  nmopnegi  32125  nmop0  32146  nmfn0  32147  adjbd1o  32245  atom1d  32513  abfmpunirn  32815  rearchi  33493  eulerpartgbij  34630  eulerpartlemgh  34636  noinfepregs  35390  subfacp1lem3  35493  dfrdg2  36104  heiborlem7  38277  qsresid  38791  cxpi11d  42913  fimgmcyc  43113  eq0rabdioph  43318  elicores  46070  liminfpnfuz  46351  xlimpnfxnegmnf2  46393  fourierdlem70  46711  fourierdlem80  46721  ovolval3  47182  rexrsb  47655  slotresfo  49481  basresposfo  49560