Theorem rexbii 2640

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	⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

Proof of Theorem rexbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 ⊢ (φ ↔ ψ)
2	1	a1i 10	. . 3 ⊢ ( ⊤ → (φ ↔ ψ))
3	2	rexbidv 2636	. 2 ⊢ ( ⊤ → (∃x ∈ A φ ↔ ∃x ∈ A ψ))
4	3	trud 1323	1 ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

Syntax hints:   ↔ wb 176   ⊤ wtru 1316  ∃wrex 2616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-rex 2621

This theorem is referenced by:  2rexbii  2642  rexanali  2661  r19.29r  2756  r19.42v  2766  r19.43  2767  rexcom13  2774  rexrot4  2775  3reeanv  2780  2ralor  2781  cbvrex2v  2845  rexcom4  2879  rexcom4a  2880  rexcom4b  2881  ceqsrex2v  2975  reu7  3032  0el  3567  uni0b  3917  iuncom  3976  iuncom4  3977  iuniin  3980  iunab  4013  iunn0  4027  iunin2  4031  iundif2  4034  iunun  4047  iunxiun  4049  iunpwss  4056  elpw12  4146  snelpw1  4147  imacok  4283  dfuni3  4316  dfint3  4319  unipw1  4326  dfaddc2  4382  addcid1  4406  nnc0suc  4413  elsuc  4414  addcass  4416  nncaddccl  4420  nndisjeq  4430  ltfinex  4465  ltfintri  4467  ncfinlowerlem1  4483  nnpw1ex  4485  evenfinex  4504  oddfinex  4505  dfevenfin2  4513  dfoddfin2  4514  evenodddisjlem1  4516  nnpweqlem1  4523  vfinspss  4552  vfinspclt  4553  vfinncsp  4555  dfphi2  4570  dfop2lem2  4575  dfop2  4576  dfproj12  4577  dfproj22  4578  proj2op  4602  phialllem1  4617  setconslem6  4737  dfima2  4746  elima3  4757  xpiundi  4818  xpiundir  4819  rexxpf  4829  iunxpf  4830  cnvuni  4896  elimapw1  4945  elimapw12  4946  elimapw13  4947  dfima4  4953  dminxp  5062  imaco  5087  coiun  5091  fnrnfv  5365  abrexco  5464  imaiun  5465  dfdm4  5508  dfrn5  5509  xpnedisj  5514  oqelins4  5795  otsnelsi3  5806  addcfnex  5825  funsex  5829  frds  5936  qsexg  5983  qsid  5991  mapexi  6004  xpassen  6058  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  enpw1pw  6076  ovmuc  6131  ovcelem1  6172  ce0nn  6181  nc0suc  6218  dflec3  6222  nclennlem1  6249  nncdiv3lem1  6276  nncdiv3lem2  6277  nncdiv3  6278  nnc3n3p1  6279  nchoicelem11  6300  nchoicelem18  6307