Theorem rexbii 2385

Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
rexbii	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem rexbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	rexbidv 2381	. 2 ⊢ (⊤ → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1298	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 103  ⊤wtru 1290  ∃wrex 2360

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-rex 2365

This theorem is referenced by:  2rexbii  2387  r19.29r  2507  r19.42v  2524  rexcom13  2532  rexrot4  2533  3reeanv  2537  cbvrex2v  2599  rexcom4  2642  rexcom4a  2643  rexcom4b  2644  ceqsrex2v  2749  reu7  2810  0el  3305  iuncom  3736  iuncom4  3737  iuniin  3740  dfiunv2  3766  iunab  3776  iunin2  3793  iundif2ss  3795  iunun  3808  iunxiun  3810  iunpwss  3820  inuni  3991  iunopab  4108  sucel  4237  iunpw  4302  xpiundi  4496  xpiundir  4497  reliin  4559  rexxpf  4583  iunxpf  4584  cnvuni  4622  dmiun  4645  dfima3  4777  rniun  4842  dminxp  4875  imaco  4936  coiun  4940  isarep1  5100  rexrn  5436  ralrn  5437  elrnrexdmb  5439  fnasrn  5475  fnasrng  5477  foima2  5530  rexima  5534  ralima  5535  abrexco  5538  imaiun  5539  fliftcnv  5574  abrexex2g  5891  abrexex2  5895  tfr1onlemaccex  6113  tfrcllemaccex  6126  tfrcldm  6128  qsid  6355  eroveu  6381  infmoti  6721  eldju  6757  genpdflem  7064  genpassl  7081  genpassu  7082  nqprm  7099  nqprrnd  7100  ltnqpr  7150  ltnqpri  7151  ltexprlemm  7157  ltexprlemopl  7158  ltexprlemopu  7160  caucvgprprlemaddq  7265  caucvgprprlem1  7266  caucvgsrlemgt1  7338  elreal  7364  axcaucvglemres  7432  dfinfre  8415  suprzclex  8842  supinfneg  9081  infsupneg  9082  ublbneg  9096  4fvwrd4  9547  caucvgre  10410  rexanuz  10417  rexfiuz  10418  resqrexlemglsq  10451  resqrexlemsqa  10453  resqrexlemex  10454  rersqreu  10457  clim0  10669  cbvsum  10745  fisum  10774  mertenslem2  10926  divalgb  11199  infssuzex  11219  bezoutlemmain  11261  bezoutlemex  11264