Theorem rexbiia 3074

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexbii  3076  rexanid  3078  2rexbiia  3190  ceqsrexbv  3613  reu8  3695  f1oweALT  7914  reldm  7986  seqomlem2  8380  fofinf1o  9241  wdom2d  9491  unbndrank  9757  cfsmolem  10183  fin1a2lem5  10317  fin1a2lem6  10318  infm3  12102  wwlktovfo  14883  even2n  16271  smndex1mnd  18802  cycsubmel  19097  znf1o  21476  lmres  23203  ist1-2  23250  itg2monolem1  25667  lhop1lem  25934  elaa  26240  ulmcau  26320  reeff1o  26373  recosf1o  26460  chpo1ubb  27408  noetainflem4  27668  bdayn0sf1o  28282  0reno  28384  istrkg2ld  28423  wlkswwlksf1o  29842  wwlksnextsurj  29863  nmopnegi  31927  nmop0  31948  nmfn0  31949  adjbd1o  32047  atom1d  32315  abfmpunirn  32609  rearchi  33296  eulerpartgbij  34342  eulerpartlemgh  34348  subfacp1lem3  35157  dfrdg2  35771  heiborlem7  37799  qsresid  38301  cxpi11d  42319  fimgmcyc  42510  eq0rabdioph  42752  elicores  45518  liminfpnfuz  45801  xlimpnfxnegmnf2  45843  fourierdlem70  46161  fourierdlem80  46171  ovolval3  46632  rexrsb  47088  slotresfo  48887  basresposfo  48966