Theorem ralbidva 2985

Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.)

Hypothesis

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

Assertion

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

Distinct variable group:   ph, x

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

Proof of Theorem ralbidva

Step	Hyp	Ref	Expression
1		ralbidva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
2	1	pm5.74da 723	. 2 |- ( ph -> ( ( x e. A -> ps ) <-> ( x e. A -> ch ) ) )
3	2	ralbidv2 2984	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   e. wcel 1990   A.wral 2912

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-ral 2917

This theorem is referenced by:  ralbidv  2986  2ralbidva  2988  raleqbidva  3154  poinxp  5182  soinxp  5183  frinxp  5184  ordunisssuc  5830  fnmptfvd  6320  funimass3  6333  fnnfpeq0  6444  cocan1  6546  cocan2  6547  isores2  6583  isoini2  6589  ofrfval  6905  ofrfval2  6915  tfindsg2  7061  f1oweALT  7152  fnsuppres  7322  dfsmo2  7444  smores  7449  smores2  7451  dfrecs3  7469  ac6sfi  8204  fimaxg  8207  ordunifi  8210  isfinite2  8218  fipreima  8272  supisolem  8379  fiming  8404  infempty  8412  ordiso2  8420  ordtypelem7  8429  cantnf  8590  wemapwe  8594  rankval3b  8689  rankonidlem  8691  iscard  8801  acndom  8874  dfac12lem3  8967  kmlem2  8973  cflim2  9085  cfsmolem  9092  ttukeylem6  9336  alephreg  9404  suplem2pr  9875  axsup  10113  sup3  10980  infm3  10982  suprleub  10989  dfinfre  11004  infregelb  11007  ofsubeq0  11017  ofsubge0  11019  zextlt  11451  prime  11458  suprfinzcl  11492  indstr  11756  supxr2  12144  supxrbnd1  12151  supxrbnd2  12152  supxrleub  12156  supxrbnd  12158  infxrgelb  12165  fzshftral  12428  mptnn0fsupp  12797  swrdeq  13444  swrdspsleq  13449  clim  14225  rlim  14226  clim2  14235  clim2c  14236  clim0c  14238  ello1mpt  14252  lo1o1  14263  o1lo1  14268  climabs0  14316  o1compt  14318  rlimdiv  14376  geomulcvg  14607  mertenslem2  14617  mertens  14618  rpnnen2lem12  14954  sqrt2irr  14979  fprodfvdvdsd  15058  fproddvdsd  15059  dfgcd2  15263  isprm7  15420  pc11  15584  pcz  15585  1arith  15631  vdwlem8  15692  vdwlem11  15695  vdw  15698  ramval  15712  pwsle  16152  mrieqvd  16298  mreacs  16319  cidpropd  16370  ismon2  16394  monpropd  16397  isepi  16400  isepi2  16401  subsubc  16513  funcres2b  16557  funcpropd  16560  isfull2  16571  isfth2  16575  fucsect  16632  fucinv  16633  pospropd  17134  ipodrsfi  17163  tsrss  17223  grpidpropd  17261  mndpropd  17316  grppropd  17437  issubg4  17613  gass  17734  gsmsymgrfixlem1  17847  gsmsymgreqlem2  17851  gexdvds  17999  gexdvds2  18000  subgpgp  18012  sylow3lem6  18047  efgval2  18137  efgsp1  18150  dprdf11  18422  subgdmdprd  18433  ringpropd  18582  abvpropd  18842  lsspropd  19017  lbspropd  19099  assapropd  19327  psrbaglefi  19372  psrbagconf1o  19374  gsumbagdiaglem  19375  mplmonmul  19464  gsumply1eq  19675  phlpropd  20000  ishil2  20063  lindfmm  20166  islindf4  20177  islindf5  20178  scmatf1  20337  cpmatmcllem  20523  cpmatmcl  20524  decpmataa0  20573  decpmatmulsumfsupp  20578  pmatcollpw2lem  20582  pm2mpmhmlem1  20623  tgss2  20791  isclo  20891  neips  20917  opnnei  20924  isperf3  20957  ssidcn  21059  lmbrf  21064  cnnei  21086  cnrest2  21090  lmss  21102  lmres  21104  ist1-2  21151  ist1-3  21153  isreg2  21181  cmpfi  21211  bwth  21213  1stccn  21266  subislly  21284  kgencn  21359  ptclsg  21418  ptcnplem  21424  xkococnlem  21462  xkoinjcn  21490  tgqtop  21515  qtopcn  21517  fbflim  21780  flimrest  21787  flfnei  21795  isflf  21797  cnflf  21806  fclsopn  21818  fclsbas  21825  fclsrest  21828  isfcf  21838  cnfcf  21846  ptcmplem3  21858  tmdgsum2  21900  eltsms  21936  tsmsgsum  21942  tsmssubm  21946  tsmsf1o  21948  utopsnneiplem  22051  ismet2  22138  prdsxmetlem  22173  elmopn2  22250  prdsbl  22296  metss  22313  metrest  22329  metcnp  22346  metcnp2  22347  metcn  22348  metucn  22376  nrginvrcn  22496  metdsge  22652  divcn  22671  elcncf2  22693  mulc1cncf  22708  cncfmet  22711  evth2  22759  lmmbr2  23057  lmmbrf  23060  iscfil2  23064  cfil3i  23067  iscau2  23075  iscau4  23077  iscauf  23078  caucfil  23081  iscmet3lem3  23088  cfilres  23094  causs  23096  lmclim  23101  rrxmet  23191  evthicc2  23229  cniccbdd  23230  ovolfioo  23236  ovolficc  23237  ismbl2  23295  mbfsup  23431  mbfinf  23432  mbflimsup  23433  0plef  23439  mbfi1flim  23490  xrge0f  23498  itg2mulclem  23513  itgeqa  23580  ellimc2  23641  ellimc3  23643  limcflf  23645  cnlimc  23652  dvferm1  23748  dvferm2  23750  rolle  23753  dvivthlem1  23771  ftc1lem6  23804  itgsubst  23812  mdegle0  23837  deg1leb  23855  plydivex  24052  ulm2  24139  ulmcaulem  24148  ulmcau  24149  ulmdvlem3  24156  abelthlem9  24194  abelth  24195  rlimcnp  24692  ftalem3  24801  issqf  24862  sqf11  24865  dvdsmulf1o  24920  dchrelbas4  24968  dchrinv  24986  2sqlem6  25148  chpo1ubb  25170  dchrmusumlema  25182  dchrisum0lema  25203  ostth3  25327  tgcgr4  25426  eqeelen  25784  brbtwn2  25785  colinearalg  25790  axcgrid  25796  axsegconlem1  25797  ax5seglem4  25812  ax5seglem5  25813  axbtwnid  25819  axpasch  25821  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem12  25855  isuvtxa  26295  uvtx2vtx1edg  26299  uvtx2vtx1edgb  26300  iscplgrnb  26312  iscplgredg  26313  vdiscusgrb  26426  uhgrvd00  26430  upgriswlk  26537  wwlksnext  26788  clwwlkinwwlk  26905  clwwlksel  26914  clwwlksf  26915  wwlksext2clwwlk  26924  wwlksubclwwlks  26925  clwlksfclwwlk  26962  numclwwlkovf2exlem2  27212  nmounbi  27631  blocnilem  27659  isph  27677  phoeqi  27713  h2hcau  27836  h2hlm  27837  hial2eq2  27964  hoeq1  28689  hoeq2  28690  adjsym  28692  cnvadj  28751  hhcno  28763  hhcnf  28764  adjvalval  28796  leop2  28983  leoptri  28995  mdbr2  29155  dmdbr2  29162  mddmd2  29168  cdj3lem3b  29299  infxrge0gelb  29531  toslublem  29667  tosglblem  29669  submarchi  29740  isarchi3  29741  cmpcref  29917  lmdvg  29999  prodindf  30085  eulerpartlemd  30428  subfacp1lem3  31164  subfacp1lem5  31166  dfrdg2  31701  sltrec  31924  opnrebl  32315  poimirlem23  33432  broucube  33443  itg2gt0cn  33465  ftc1cnnc  33484  lmclim2  33554  caures  33556  sstotbnd2  33573  rrnmet  33628  rrncmslem  33631  isdrngo3  33758  isidlc  33814  cvrval2  34561  isat3  34594  iscvlat2N  34611  glbconN  34663  ltrneq  35435  cdlemefrs29clN  35687  cdlemefrs32fva  35688  cdleme32fva  35725  cdlemk33N  36197  cdlemk34  36198  cdlemkid3N  36221  cdlemkid4  36222  diaglbN  36344  dibglbN  36455  dihglbcpreN  36589  dihglblem6  36629  hdmap1eulem  37113  hdmap1eulemOLDN  37114  hdmapoc  37223  hlhilocv  37249  wepwsolem  37612  fnwe2lem2  37621  islnm2  37648  clsk3nimkb  38338  ntrclsneine0  38363  ntrneineine0  38385  ntrneineine1  38386  ntrneicls00  38387  ntrneicls11  38388  ntrneiiso  38389  ntrneik2  38390  ntrneix2  38391  ntrneikb  38392  ntrneixb  38393  ntrneik3  38394  ntrneix3  38395  ntrneik13  38396  ntrneix13  38397  ntrneik4w  38398  ntrneik4  38399  caofcan  38522  infxrbnd2  39585  supminfxr  39694  evthiccabs  39718  ellimcabssub0  39849  climf  39854  clim2f  39868  clim2cf  39882  clim0cf  39886  limsupmnflem  39952  limsupre2lem  39956  limsupreuzmpt  39971  supcnvlimsup  39972  limsupge  39993  liminfreuzlem  40034  liminfltlem  40036  liminflimsupclim  40039  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem80  40403  fourierdlem83  40406  fourierdlem87  40410  voliunsge0lem  40689  meaiuninclem  40697  hoidmv1lelem3  40807  hoidmvlelem4  40812  hoidmvlelem5  40813  issmflem  40936  pfxeq  41404  islinindfis  42238  elbigolo1  42351  aacllem  42547