Theorem rexbidva 3049

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.)

Hypothesis

Ref	Expression
rexbidva.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )

Assertion

Ref	Expression
rexbidva	|- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		rexbidva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
2	1	pm5.32da 673	. 2 |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. A /\ ch ) ) )
3	2	rexbidv2 3048	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-rex 2918

This theorem is referenced by:  rexbidv  3052  2rexbiia  3055  2rexbidva  3056  rexeqbidva  3155  frinxp  5184  onfr  5763  dfimafn  6245  funimass4  6247  fliftel  6559  fliftf  6565  isomin  6587  f1oiso  6601  releldm2  7218  oaass  7641  qsinxp  7823  qliftel  7830  fimaxg  8207  ordunifi  8210  supisolem  8379  fiming  8404  wemapwe  8594  cflim2  9085  cfsmolem  9092  alephsing  9098  brdom7disj  9353  brdom6disj  9354  alephreg  9404  nqereu  9751  1idpr  9851  map2psrpr  9931  axsup  10113  rereccl  10743  sup3  10980  infm3  10982  supadd  10991  creur  11014  creui  11015  nndiv  11061  nnrecl  11290  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  supxrbnd1  12151  supxrbnd2  12152  supxrbnd  12158  rabssnn0fi  12785  mptnn0fsupp  12797  expnlbnd  12994  wrdl3s3  13705  limsuplt  14210  clim2  14235  clim2c  14236  clim0c  14238  ello12  14247  elo12  14258  rlimresb  14296  climabs0  14316  sumeq2ii  14423  mertens  14618  prodeq2ii  14643  zprod  14667  nndivides  14990  alzdvds  15042  oddm1even  15067  oddnn02np1  15072  oddge22np1  15073  evennn02n  15074  evennn2n  15075  divalglem4  15119  divalgb  15127  modremain  15132  modprmn0modprm0  15512  vdwlem6  15690  vdwlem11  15695  vdw  15698  ramval  15712  imasleval  16201  dfiso3  16433  fullestrcsetc  16791  fullsetcestrc  16806  isipodrs  17161  ipodrsfi  17163  gsumpropd2lem  17273  mndpropd  17316  grppropd  17437  conjnmzb  17695  symgextfo  17842  symgfixfo  17859  sylow1lem2  18014  sylow3lem1  18042  sylow3lem3  18044  lsmelvalm  18066  lsmass  18083  iscyg3  18288  ghmcyg  18297  cycsubgcyg  18302  pgpfac1lem2  18474  pgpfac1lem4  18477  ablfac2  18488  dvdsr02  18656  crngunit  18662  dvdsrpropd  18696  lpigen  19256  znunit  19912  elfilspd  20142  scmatmats  20317  symgmatr01  20460  isclo  20891  iscnp3  21048  lmbrf  21064  cncnp  21084  lmss  21102  isnrm2  21162  cmpfi  21211  1stcfb  21248  1stccnp  21265  ptrescn  21442  txkgen  21455  xkoinjcn  21490  trfil3  21692  fmid  21764  lmflf  21809  txflf  21810  ptcmplem3  21858  tsmsf1o  21948  ucnprima  22086  metrest  22329  metcnp  22346  metcnp2  22347  txmetcnp  22352  metuel2  22370  metustbl  22371  psmetutop  22372  metucn  22376  evth2  22759  lmmbrf  23060  iscfil2  23064  fmcfil  23070  iscau2  23075  iscau4  23077  iscauf  23078  caucfil  23081  iscmet3lem3  23088  cfilresi  23093  causs  23096  lmclim  23101  ivth2  23224  ovolfioo  23236  ovolficc  23237  ovolshftlem1  23277  ovolscalem1  23281  volsup2  23373  ismbf3d  23421  mbfaddlem  23427  mbfsup  23431  mbfinf  23432  itg2seq  23509  itg2gt0  23527  ellimc2  23641  ellimc3  23643  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvivth  23773  lhop1lem  23776  deg1ldg  23852  ulm2  24139  ulmdvlem3  24156  dcubic  24573  mcubic  24574  cubic2  24575  rlimcnp  24692  ftalem3  24801  isppw2  24841  lgsquadlem2  25106  2lgslem1a  25116  dchrmusumlema  25182  dchrisum0lema  25203  tglowdim2l  25545  mirreu3  25549  oppcom  25636  iscgra1  25702  axsegcon  25807  axpasch  25821  axcontlem7  25850  usgr2pth0  26661  usgr2wspthon  26858  elwwlks2  26861  elwspths2spth  26862  rusgrnumwwlks  26869  clwwlksfo  26918  eclclwwlksn1  26952  eucrctshift  27103  fusgreg2wsp  27200  nmobndi  27630  nmounbi  27631  nmoo0  27646  h2hcau  27836  h2hlm  27837  shsel3  28174  pjhtheu2  28275  chscllem2  28497  adjbdln  28942  branmfn  28964  pjimai  29035  chrelati  29223  cdj3lem3  29297  cdj3lem3b  29299  dfimafnf  29436  ofpreima  29465  isarchi2  29739  submarchi  29740  archirng  29742  archiabl  29752  isarchiofld  29817  ordtconnlem1  29970  lmdvg  29999  esumfsup  30132  dya2icoseg2  30340  eulerpartlemgh  30440  ballotlemodife  30559  ballotlemsima  30577  erdszelem10  31182  iscvm  31241  elintfv  31662  wsuclem  31773  wsuclemOLD  31774  etasslt  31920  seglelin  32223  outsideofeu  32238  opnrebl  32315  opnrebl2  32316  filnetlem4  32376  bj-finsumval0  33147  phpreu  33393  ptrest  33408  poimirlem3  33412  poimirlem4  33413  poimirlem17  33426  poimirlem26  33435  poimirlem27  33436  broucube  33443  mblfinlem1  33446  lmclim2  33554  caures  33556  isbnd3b  33584  heiborlem7  33616  heiborlem10  33619  rrncmslem  33631  isdrngo2  33757  prter3  34167  islshpsm  34267  lsatfixedN  34296  lrelat  34301  eqlkr2  34387  lshpkrlem1  34397  lfl1dim  34408  eqlkr4  34452  ishlat3N  34641  hlsupr2  34673  hlrelat5N  34687  hlrelat  34688  cvrval5  34701  cvrat42  34730  athgt  34742  3dim0  34743  islln3  34796  llnexatN  34807  islpln3  34819  islvol3  34862  islvol5  34865  isline4N  35063  polval2N  35192  4atex3  35367  cdleme0ex2N  35511  cdlemefrs29cpre1  35686  cdlemb3  35894  cdlemg33c  35996  cdlemg33e  35998  dia1dim2  36351  cdlemm10N  36407  dib1dim2  36457  diclspsn  36483  dih1dimatlem  36618  dihatexv2  36628  djhcvat42  36704  dihjat1lem  36717  dvh4dimat  36727  dvh2dimatN  36729  lcfrlem9  36839  mapdval4N  36921  mapdcv  36949  elrfirn  37258  elrfirn2  37259  mrefg3  37271  diophin  37336  diophun  37337  diophren  37377  rmxycomplete  37482  wepwsolem  37612  fnwe2lem2  37621  islssfg  37640  ntrneineine0lem  38381  ntrneineine1lem  38382  ntrneiel2  38384  extoimad  38464  supsubc  39569  infxrbnd2  39585  supminfxr  39694  evthiccabs  39718  elicores  39760  clim2f  39868  clim2cf  39882  clim0cf  39886  clim2f2  39902  limsupub  39936  limsupmnflem  39952  limsupre2lem  39956  limsuplt2  39985  liminfreuzlem  40034  liminfltlem  40036  liminflimsupclim  40039  xlimmnfmpt  40069  xlimpnfmpt  40070  fourierdlem73  40396  fourierdlem83  40406  ovolval2  40858  dfaimafn  41245  iccelpart  41369  fmtnoprmfac1  41477  fmtnoprmfac2  41479  fmtnofac2lem  41480  dfeven2  41562  dfodd3  41563  sprsymrelf  41745  sprsymrelfo  41747  uspgrsprfo  41756  elbigo2  42346