Theorem rexbiia 3085

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

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2119  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexbii  3087  rexanid  3089  2rexbiia  3201  ceqsrexbv  3601  reu8  3681  f1oweALT  7921  reldm  7993  seqomlem2  8387  fofinf1o  9239  wdom2d  9492  unbndrank  9764  cfsmolem  10190  fin1a2lem5  10324  fin1a2lem6  10325  infm3  12113  wwlktovfo  14918  even2n  16309  smndex1mnd  18879  cycsubmel  19173  znf1o  21533  lmres  23290  ist1-2  23337  itg2monolem1  25742  lhop1lem  26005  elaa  26307  ulmcau  26385  reeff1o  26437  recosf1o  26524  chpo1ubb  27469  noetainflem4  27729  bdayn0sf1o  28387  istrkg2ld  28553  wlkswwlksf1o  29972  wwlksnextsurj  29993  nmopnegi  32061  nmop0  32082  nmfn0  32083  adjbd1o  32181  atom1d  32449  abfmpunirn  32751  rearchi  33436  eulerpartgbij  34563  eulerpartlemgh  34569  noinfepregs  35321  subfacp1lem3  35417  dfrdg2  36028  heiborlem7  38191  qsresid  38705  cxpi11d  42827  fimgmcyc  43027  eq0rabdioph  43232  elicores  45985  liminfpnfuz  46266  xlimpnfxnegmnf2  46308  fourierdlem70  46626  fourierdlem80  46636  ovolval3  47097  rexrsb  47570  slotresfo  49396  basresposfo  49475