Theorem rexbiia 3077

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2111  ∃wrex 3056

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  rexbii  3079  rexanid  3081  2rexbiia  3193  ceqsrexbv  3611  reu8  3692  f1oweALT  7904  reldm  7976  seqomlem2  8370  fofinf1o  9216  wdom2d  9466  unbndrank  9735  cfsmolem  10161  fin1a2lem5  10295  fin1a2lem6  10296  infm3  12081  wwlktovfo  14865  even2n  16253  smndex1mnd  18818  cycsubmel  19113  znf1o  21489  lmres  23216  ist1-2  23263  itg2monolem1  25679  lhop1lem  25946  elaa  26252  ulmcau  26332  reeff1o  26385  recosf1o  26472  chpo1ubb  27420  noetainflem4  27680  bdayn0sf1o  28296  0reno  28400  istrkg2ld  28439  wlkswwlksf1o  29858  wwlksnextsurj  29879  nmopnegi  31943  nmop0  31964  nmfn0  31965  adjbd1o  32063  atom1d  32331  abfmpunirn  32632  rearchi  33309  eulerpartgbij  34383  eulerpartlemgh  34389  subfacp1lem3  35224  dfrdg2  35835  heiborlem7  37863  qsresid  38365  cxpi11d  42382  fimgmcyc  42573  eq0rabdioph  42815  elicores  45579  liminfpnfuz  45860  xlimpnfxnegmnf2  45902  fourierdlem70  46220  fourierdlem80  46230  ovolval3  46691  rexrsb  47137  slotresfo  48936  basresposfo  49015