Theorem rexbiia 3098

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexbii  3100  rexanid  3102  2rexbiia  3224  ceqsrexbv  3669  reu8  3755  f1oweALT  8013  reldm  8085  seqomlem2  8507  fofinf1o  9400  wdom2d  9649  unbndrank  9911  cfsmolem  10339  fin1a2lem5  10473  fin1a2lem6  10474  infm3  12254  wwlktovfo  15007  even2n  16390  smndex1mnd  18945  cycsubmel  19240  znf1o  21593  lmres  23329  ist1-2  23376  itg2monolem1  25805  lhop1lem  26072  elaa  26376  ulmcau  26456  reeff1o  26509  recosf1o  26595  chpo1ubb  27543  noetainflem4  27803  0reno  28447  istrkg2ld  28486  wlkswwlksf1o  29912  wwlksnextsurj  29933  nmopnegi  31997  nmop0  32018  nmfn0  32019  adjbd1o  32117  atom1d  32385  abfmpunirn  32670  rearchi  33339  eulerpartgbij  34337  eulerpartlemgh  34343  subfacp1lem3  35150  dfrdg2  35759  heiborlem7  37777  qsresid  38281  cxpi11d  42331  fimgmcyc  42489  eq0rabdioph  42732  elicores  45451  liminfpnfuz  45737  xlimpnfxnegmnf2  45779  fourierdlem70  46097  fourierdlem80  46107  ovolval3  46568  rexrsb  47015