Theorem rexbiia 3090

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2106  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-rex 3069

This theorem is referenced by:  rexbii  3092  rexanid  3094  2rexbiia  3216  ceqsrexbv  3656  reu8  3742  f1oweALT  7996  reldm  8068  seqomlem2  8490  fofinf1o  9370  wdom2d  9618  unbndrank  9880  cfsmolem  10308  fin1a2lem5  10442  fin1a2lem6  10443  infm3  12225  wwlktovfo  14994  even2n  16376  smndex1mnd  18936  cycsubmel  19231  znf1o  21588  lmres  23324  ist1-2  23371  itg2monolem1  25800  lhop1lem  26067  elaa  26373  ulmcau  26453  reeff1o  26506  recosf1o  26592  chpo1ubb  27540  noetainflem4  27800  0reno  28444  istrkg2ld  28483  wlkswwlksf1o  29909  wwlksnextsurj  29930  nmopnegi  31994  nmop0  32015  nmfn0  32016  adjbd1o  32114  atom1d  32382  abfmpunirn  32669  rearchi  33354  eulerpartgbij  34354  eulerpartlemgh  34360  subfacp1lem3  35167  dfrdg2  35777  heiborlem7  37804  qsresid  38307  cxpi11d  42358  fimgmcyc  42521  eq0rabdioph  42764  elicores  45486  liminfpnfuz  45772  xlimpnfxnegmnf2  45814  fourierdlem70  46132  fourierdlem80  46142  ovolval3  46603  rexrsb  47050