NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  rexbii GIF version

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
StepHypRef Expression
1 ralbii.1 . . . 4 (φψ)
21a1i 10 . . 3 ( ⊤ → (φψ))
32rexbidv 2635 . 2 ( ⊤ → (x A φx A ψ))
43trud 1323 1 (x A φx A ψ)
Colors of variables: wff setvar class
Syntax hints:  wb 176  wtru 1316  wrex 2615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  6247  nncdiv3lem1  6273  nncdiv3lem2  6274  nncdiv3  6275  nnc3n3p1  6276  nchoicelem11  6297  nchoicelem18  6304
  Copyright terms: Public domain W3C validator