Theorem rexbii 2557

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 2551	. 2 ⊢ (⊤ → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1411	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   ↔ wb 105  ⊤wtru 1403  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-rex 2534

This theorem is used by:  2rexbii  2559  r19.29r  2689  r19.42v  2708  rexcom13  2717  rexrot4  2718  3reeanv  2722  cbvrex2vw  2798  cbvrex2v  2800  rexcom4  2845  rexcom4a  2846  rexcom4b  2847  ceqsrex2v  2958  clel5  2963  reu7  3021  0el  3544  iuncom  4018  iuncom4  4019  iuniin  4022  dfiunv2  4048  iunab  4059  iunin2  4076  iundif2ss  4078  iunun  4091  iunxiun  4094  iunpwss  4104  inuni  4291  iunopab  4424  sucel  4555  iunpw  4626  xpiundi  4833  xpiundir  4834  reliin  4899  rexxpf  4927  iunxpf  4928  cnvuni  4966  dmiun  4990  dfima3  5129  rniun  5198  dminxp  5232  imaco  5293  coiun  5297  isarep1  5467  rexrn  5845  ralrn  5846  elrnrexdmb  5848  fnasrn  5887  fnasrng  5889  foima2  5957  rexima  5960  ralima  5961  abrexco  5965  imaiun  5966  fliftcnv  6001  abrexex2g  6349  abrexex2  6353  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcldm  6634  qsid  6874  eroveu  6900  ixp0  7013  infmoti  7368  eldju  7408  ficardon  7534  genpdflem  7874  genpassl  7891  genpassu  7892  nqprm  7909  nqprrnd  7910  ltnqpr  7960  ltnqpri  7961  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  caucvgprprlemaddq  8075  caucvgprprlem1  8076  suplocexprlemml  8083  suplocexprlemloc  8088  caucvgsrlemgt1  8162  elreal  8195  axcaucvglemres  8266  axpre-suploc  8269  dfinfre  9287  suprzclex  9746  supinfneg  9997  infsupneg  9998  ublbneg  10015  4fvwrd4  10549  infssuzex  10668  caucvgre  11749  rexanuz  11756  rexfiuz  11757  resqrexlemglsq  11790  resqrexlemsqa  11792  resqrexlemex  11793  rersqreu  11796  clim0  12053  cbvsum  12128  fsum3  12156  mertenslem2  12305  cbvprod  12327  fprodseq  12352  divalgb  12694  bezoutlemmain  12777  bezoutlemex  12780  pythagtriplem2  13047  pythagtriplem19  13063  pythagtrip  13064  pceu  13076  ennnfoneleminc  13304  ennnfonelemex  13307  ennnfonelemr  13316  imasaddfnlemg  13637  tgval2  15154  ntreq0  15235  metrest  15609  plyun0  15839  clwwlknun  16694  ralsbii  17154