Theorem rexbiia 3107

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexbii  3109  rexanid  3111  2rexbiia  3223  ceqsrexbv  3609  reu8  3690  f1oweALT  7985  reldm  8056  seqomlem2  8465  fofinf1o  9325  wdom2d  9578  unbndrank  9859  cfsmolem  10352  fin1a2lem5  10486  fin1a2lem6  10487  infm3  12280  wwlktovfo  15117  even2n  16518  smndex1mnd  19115  cycsubmel  19421  znf1o  21863  lmres  23624  ist1-2  23671  itg2monolem1  26077  lhop1lem  26339  elaa  26645  ulmcau  26728  reeff1o  26780  recosf1o  26869  chpo1ubb  27814  noetainflem4  28103  bdayn0sf1o  28762  istrkg2ld  28928  wlkswwlksf1o  30474  wwlksnextsurj  30495  nmopnegi  32573  nmop0  32594  nmfn0  32595  adjbd1o  32693  atom1d  32961  abfmpunirn  33294  rearchi  33954  eulerpartgbij  35051  eulerpartlemgh  35057  noinfepregs  35858  subfacp1lem3  36034  dfrdg2  36650  heiborlem7  38845  qsresid  39357  cxpi11d  43488  fimgmcyc  43692  eq0rabdioph  43881  elicores  46639  liminfpnfuz  46920  xlimpnfxnegmnf2  46962  fourierdlem70  47280  fourierdlem80  47290  ovolval3  47751  rexrsb  48264  slotresfo  50107  basresposfo  50186