Theorem rexbii 2639

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 2635	. 2 ⊢ ( ⊤ → (∃x ∈ A φ ↔ ∃x ∈ A ψ))
4	3	trud 1323	1 ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

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

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 2620

This theorem is referenced by:  2rexbii  2641  rexanali  2660  r19.29r  2755  r19.42v  2765  r19.43  2766  rexcom13  2773  rexrot4  2774  3reeanv  2779  2ralor  2780  cbvrex2v  2844  rexcom4  2878  rexcom4a  2879  rexcom4b  2880  ceqsrex2v  2974  reu7  3031  0el  3566  uni0b  3916  iuncom  3975  iuncom4  3976  iuniin  3979  iunab  4012  iunn0  4026  iunin2  4030  iundif2  4033  iunun  4046  iunxiun  4048  iunpwss  4055  elpw12  4145  snelpw1  4146  imacok  4282  dfuni3  4315  dfint3  4318  unipw1  4325  dfaddc2  4381  addcid1  4405  nnc0suc  4412  elsuc  4413  addcass  4415  nncaddccl  4419  nndisjeq  4429  ltfinex  4464  ltfintri  4466  ncfinlowerlem1  4482  nnpw1ex  4484  evenfinex  4503  oddfinex  4504  dfevenfin2  4512  dfoddfin2  4513  evenodddisjlem1  4515  nnpweqlem1  4522  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  dfphi2  4569  dfop2lem2  4574  dfop2  4575  dfproj12  4576  dfproj22  4577  proj2op  4601  phialllem1  4616  setconslem6  4736  dfima2  4745  elima3  4756  xpiundi  4817  xpiundir  4818  rexxpf  4828  iunxpf  4829  cnvuni  4895  elimapw1  4944  elimapw12  4945  elimapw13  4946  dfima4  4952  dminxp  5061  imaco  5086  coiun  5090  fnrnfv  5364  abrexco  5463  imaiun  5464  dfdm4  5507  dfrn5  5508  xpnedisj  5513  oqelins4  5794  otsnelsi3  5805  addcfnex  5824  funsex  5828  frds  5935  qsexg  5982  qsid  5990  mapexi  6003  xpassen  6057  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  enpw1pw  6075  ovmuc  6130  ovcelem1  6171  ce0nn  6180  nc0suc  6217  dflec3  6221  nclennlem1  6248  nncdiv3lem1  6275  nncdiv3lem2  6276  nncdiv3  6277  nnc3n3p1  6278  nchoicelem11  6299  nchoicelem18  6306