Theorem ralbidva 2968

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	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ralbidva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidva

Step	Hyp	Ref	Expression
1		ralbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.74da 719	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜒)))
3	2	ralbidv2 2967	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901

This theorem is referenced by:  ralbidv  2969  2ralbidva  2971  raleqbidva  3131  poinxp  5105  soinxp  5106  frinxp  5107  ordunisssuc  5747  fnmptfvd  6228  funimass3  6241  fnnfpeq0  6349  cocan1  6446  cocan2  6447  isores2  6483  isoini2  6489  ofrfval  6803  ofrfval2  6813  tfindsg2  6953  f1oweALT  7043  fnsuppres  7209  dfsmo2  7331  smores  7336  smores2  7338  dfrecs3  7356  ac6sfi  8089  fimaxg  8092  ordunifi  8095  isfinite2  8103  fipreima  8155  supisolem  8262  fiming  8287  infempty  8295  ordiso2  8303  ordtypelem7  8312  cantnf  8473  wemapwe  8477  rankval3b  8572  rankonidlem  8574  iscard  8684  acndom  8757  dfac12lem3  8850  kmlem2  8856  cflim2  8968  cfsmolem  8975  ttukeylem6  9219  alephreg  9283  suplem2pr  9754  axsup  9992  sup3  10859  infm3  10861  suprleub  10866  dfinfre  10881  infregelb  10884  ofsubeq0  10894  ofsubge0  10896  zextlt  11327  prime  11334  suprfinzcl  11368  indstr  11632  supxr2  12016  supxrbnd1  12023  supxrbnd2  12024  supxrleub  12028  supxrbnd  12030  infxrgelb  12037  fzshftral  12297  mptnn0fsupp  12659  swrdeq  13296  swrdspsleq  13301  clim  14073  rlim  14074  clim2  14083  clim2c  14084  clim0c  14086  ello1mpt  14100  lo1o1  14111  o1lo1  14116  climabs0  14164  o1compt  14166  rlimdiv  14224  geomulcvg  14446  mertenslem2  14456  mertens  14457  rpnnen2lem12  14793  sqrt2irr  14817  fprodfvdvdsd  14896  fproddvdsd  14897  dfgcd2  15101  isprm7  15258  pc11  15422  pcz  15423  1arith  15469  vdwlem8  15530  vdwlem11  15533  vdw  15536  ramval  15550  pwsle  15975  mrieqvd  16121  mreacs  16142  cidpropd  16193  ismon2  16217  monpropd  16220  isepi  16223  isepi2  16224  subsubc  16336  funcres2b  16380  funcpropd  16383  isfull2  16394  isfth2  16398  fucsect  16455  fucinv  16456  pospropd  16957  ipodrsfi  16986  tsrss  17046  grpidpropd  17084  mndpropd  17139  grppropd  17260  issubg4  17436  gass  17557  gsmsymgrfixlem1  17670  gsmsymgreqlem2  17674  gexdvds  17822  gexdvds2  17823  subgpgp  17835  sylow3lem6  17870  efgval2  17960  efgsp1  17973  dprdf11  18245  subgdmdprd  18256  ringpropd  18405  abvpropd  18665  lsspropd  18838  lbspropd  18920  assapropd  19148  psrbaglefi  19193  psrbagconf1o  19195  gsumbagdiaglem  19196  mplmonmul  19285  gsumply1eq  19496  phlpropd  19819  ishil2  19882  lindfmm  19985  islindf4  19996  islindf5  19997  scmatf1  20156  cpmatmcllem  20342  cpmatmcl  20343  decpmataa0  20392  decpmatmulsumfsupp  20397  pmatcollpw2lem  20401  pm2mpmhmlem1  20442  tgss2  20602  isclo  20701  neips  20727  opnnei  20734  isperf3  20767  ssidcn  20869  lmbrf  20874  cnnei  20896  cnrest2  20900  lmss  20912  lmres  20914  ist1-2  20961  ist1-3  20963  isreg2  20991  cmpfi  21021  bwth  21023  1stccn  21076  subislly  21094  kgencn  21169  ptclsg  21228  ptcnplem  21234  xkococnlem  21272  xkoinjcn  21300  tgqtop  21325  qtopcn  21327  fbflim  21590  flimrest  21597  flfnei  21605  isflf  21607  cnflf  21616  fclsopn  21628  fclsbas  21635  fclsrest  21638  isfcf  21648  cnfcf  21656  ptcmplem3  21668  tmdgsum2  21710  eltsms  21746  tsmsgsum  21752  tsmssubm  21756  tsmsf1o  21758  utopsnneiplem  21861  ismet2  21948  prdsxmetlem  21983  elmopn2  22060  prdsbl  22106  metss  22123  metrest  22139  metcnp  22156  metcnp2  22157  metcn  22158  metucn  22186  nrginvrcn  22306  metdsge  22460  divcn  22479  elcncf2  22501  mulc1cncf  22516  cncfmet  22519  evth2  22567  lmmbr2  22865  lmmbrf  22868  iscfil2  22872  cfil3i  22875  iscau2  22883  iscau4  22885  iscauf  22886  caucfil  22889  iscmet3lem3  22896  cfilres  22902  causs  22904  lmclim  22909  rrxmet  22999  evthicc2  23036  cniccbdd  23037  ovolfioo  23043  ovolficc  23044  ismbl2  23102  mbfsup  23237  mbfinf  23238  mbflimsup  23239  0plef  23245  mbfi1flim  23296  xrge0f  23304  itg2mulclem  23319  itgeqa  23386  ellimc2  23447  ellimc3  23449  limcflf  23451  cnlimc  23458  dvferm1  23552  dvferm2  23554  rolle  23557  dvivthlem1  23575  ftc1lem6  23608  itgsubst  23616  mdegle0  23641  deg1leb  23659  plydivex  23856  ulm2  23943  ulmcaulem  23952  ulmcau  23953  ulmdvlem3  23960  abelthlem9  23998  abelth  23999  rlimcnp  24492  ftalem3  24601  issqf  24662  sqf11  24665  dvdsmulf1o  24720  dchrelbas4  24768  dchrinv  24786  2sqlem6  24948  chpo1ubb  24970  dchrmusumlema  24982  dchrisum0lema  25003  ostth3  25127  tgcgr4  25226  eqeelen  25584  brbtwn2  25585  colinearalg  25590  axcgrid  25596  axsegconlem1  25597  ax5seglem4  25612  ax5seglem5  25613  axbtwnid  25619  axpasch  25621  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem12  25655  wwlknext  26252  clwwlkel  26321  clwwlkf  26322  wwlkext2clwwlk  26331  wwlksubclwwlk  26332  clwlkfclwwlk  26371  extwwlkfablem2  26605  numclwwlkovf2ex  26613  nmounbi  27015  blocnilem  27043  isph  27061  phoeqi  27097  h2hcau  27220  h2hlm  27221  hial2eq2  27348  hoeq1  28073  hoeq2  28074  adjsym  28076  cnvadj  28135  hhcno  28147  hhcnf  28148  adjvalval  28180  leop2  28367  leoptri  28379  mdbr2  28539  dmdbr2  28546  mddmd2  28552  cdj3lem3b  28683  infxrge0gelb  28921  toslublem  28998  tosglblem  29000  submarchi  29071  isarchi3  29072  cmpcref  29245  lmdvg  29327  eulerpartlemd  29755  subfacp1lem3  30418  subfacp1lem5  30420  dfrdg2  30945  opnrebl  31485  poimirlem23  32602  broucube  32613  itg2gt0cn  32635  ftc1cnnc  32654  lmclim2  32724  caures  32726  sstotbnd2  32743  rrnmet  32798  rrncmslem  32801  isdrngo3  32928  isidlc  32984  cvrval2  33579  isat3  33612  iscvlat2N  33629  glbconN  33681  ltrneq  34453  cdlemefrs29clN  34705  cdlemefrs32fva  34706  cdleme32fva  34743  cdlemk33N  35215  cdlemk34  35216  cdlemkid3N  35239  cdlemkid4  35240  diaglbN  35362  dibglbN  35473  dihglbcpreN  35607  dihglblem6  35647  hdmap1eulem  36131  hdmap1eulemOLDN  36132  hdmapoc  36241  hlhilocv  36267  wepwsolem  36630  fnwe2lem2  36639  islnm2  36666  clsk3nimkb  37358  ntrclsneine0  37383  ntrneineine0  37405  ntrneineine1  37406  ntrneicls00  37407  ntrneicls11  37408  ntrneiiso  37409  ntrneik2  37410  ntrneix2  37411  ntrneikb  37412  ntrneixb  37413  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  ntrneik4w  37418  ntrneik4  37419  caofcan  37544  infxrbnd2  38526  evthiccabs  38565  ellimcabssub0  38684  climf  38689  clim2f  38703  clim2cf  38717  clim0cf  38721  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem80  39079  fourierdlem83  39082  fourierdlem87  39086  voliunsge0lem  39365  meaiuninclem  39373  hoidmv1lelem3  39483  hoidmvlelem4  39488  hoidmvlelem5  39489  issmflem  39613  pfxeq  40267  isuvtxa  40621  uvtx2vtx1edg  40625  uvtx2vtx1edgb  40626  iscplgrnb  40638  iscplgredg  40639  vdiscusgrb  40746  uhgrvd00  40750  wwlksnext  41099  clwwlksel  41221  clwwlksf  41222  wwlksext2clwwlk  41231  wwlksubclwwlks  41232  clwlksfclwwlk  41269  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  islinindfis  42032  elbigolo1  42149  aacllem  42356