Theorem rexbiia 3078

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  ∃wrex 3057

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  rexbii  3080  rexanid  3082  2rexbiia  3194  ceqsrexbv  3607  reu8  3688  f1oweALT  7912  reldm  7984  seqomlem2  8378  fofinf1o  9225  wdom2d  9475  unbndrank  9744  cfsmolem  10170  fin1a2lem5  10304  fin1a2lem6  10305  infm3  12090  wwlktovfo  14869  even2n  16257  smndex1mnd  18822  cycsubmel  19116  znf1o  21492  lmres  23218  ist1-2  23265  itg2monolem1  25681  lhop1lem  25948  elaa  26254  ulmcau  26334  reeff1o  26387  recosf1o  26474  chpo1ubb  27422  noetainflem4  27682  bdayn0sf1o  28298  0reno  28402  istrkg2ld  28441  wlkswwlksf1o  29861  wwlksnextsurj  29882  nmopnegi  31949  nmop0  31970  nmfn0  31971  adjbd1o  32069  atom1d  32337  abfmpunirn  32638  rearchi  33320  eulerpartgbij  34408  eulerpartlemgh  34414  subfacp1lem3  35249  dfrdg2  35860  heiborlem7  37880  qsresid  38386  cxpi11d  42464  fimgmcyc  42655  eq0rabdioph  42896  elicores  45660  liminfpnfuz  45941  xlimpnfxnegmnf2  45983  fourierdlem70  46301  fourierdlem80  46311  ovolval3  46772  rexrsb  47227  slotresfo  49026  basresposfo  49105