Theorem ralbidva 3112

Description: Formula-building rule for restricted universal quantifier (deduction form). (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 801	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜒)))
3	2	ralbidv2 3111	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3070

This theorem is referenced by:  ralbidv  3113  2ralbidva  3129  raleqbidva  3355  poinxp  5668  soinxp  5669  frinxp  5670  ordunisssuc  6372  fnmptfvd  6927  funimass3  6940  fnnfpeq0  7059  cocan1  7172  cocan2  7173  isores2  7213  isoini2  7219  ofrfvalg  7550  ofrfval2  7563  tfindsg2  7717  f1oweALT  7824  fnsuppres  8016  dfsmo2  8187  smores  8192  smores2  8194  dfrecs3  8212  dfrecs3OLD  8213  ac6sfi  9067  fimaxg  9070  ordunifi  9073  isfinite2  9081  fipreima  9134  supisolem  9241  fiming  9266  infempty  9275  ordiso2  9283  ordtypelem7  9292  cantnf  9460  wemapwe  9464  rankval3b  9593  rankonidlem  9595  iscard  9742  acndom  9816  dfac12lem3  9910  kmlem2  9916  cflim2  10028  cfsmolem  10035  ttukeylem6  10279  alephreg  10347  suplem2pr  10818  axsup  11059  sup3  11941  infm3  11943  suprleub  11950  dfinfre  11965  infregelb  11968  ofsubeq0  11979  ofsubge0  11981  zextlt  12403  prime  12410  suprfinzcl  12445  indstr  12665  supxr2  13057  supxrbnd1  13064  supxrbnd2  13065  supxrleub  13069  supxrbnd  13071  infxrgelb  13078  fzshftral  13353  mptnn0fsupp  13726  swrdspsleq  14387  pfxeq  14418  clim  15212  rlim  15213  clim2  15222  clim2c  15223  clim0c  15225  ello1mpt  15239  lo1o1  15250  o1lo1  15255  climabs0  15303  o1compt  15305  rlimdiv  15366  geomulcvg  15597  mertenslem2  15606  mertens  15607  rpnnen2lem12  15943  sqrt2irr  15967  fprodfvdvdsd  16052  fproddvdsd  16053  dfgcd2  16263  isprm7  16422  pc11  16590  pcz  16591  1arith  16637  vdwlem8  16698  vdwlem11  16701  vdw  16704  ramval  16718  pwsle  17212  mrieqvd  17356  mreacs  17376  cidpropd  17428  ismon2  17455  monpropd  17458  isepi  17461  isepi2  17462  subsubc  17577  funcres2b  17621  funcpropd  17625  isfull2  17636  isfth2  17640  fucsect  17699  fucinv  17700  pospropd  18054  ipodrsfi  18266  tsrss  18316  grpidpropd  18355  mndpropd  18419  smndex1mnd  18558  grppropd  18603  issubg4  18783  gass  18916  gsmsymgrfixlem1  19044  gsmsymgreqlem2  19048  gexdvds  19198  gexdvds2  19199  subgpgp  19211  sylow3lem6  19246  efgval2  19339  efgsp1  19352  dprdf11  19635  subgdmdprd  19646  ringpropd  19830  abvpropd  20111  lsspropd  20288  lbspropd  20370  phlpropd  20869  ishil2  20935  frlmplusgvalb  20985  frlmvscavalb  20986  frlmvplusgscavalb  20987  lindfmm  21043  islindf4  21054  islindf5  21055  assapropd  21085  psrbaglefi  21144  psrbaglefiOLD  21145  psrbagconf1o  21148  psrbagconf1oOLD  21149  gsumbagdiaglemOLD  21150  gsumbagdiaglem  21153  mplmonmul  21246  gsumply1eq  21485  scmatf1  21689  cpmatmcllem  21876  cpmatmcl  21877  decpmataa0  21926  decpmatmulsumfsupp  21931  pmatcollpw2lem  21935  pm2mpmhmlem1  21976  tgss2  22146  isclo  22247  neips  22273  opnnei  22280  isperf3  22313  ssidcn  22415  lmbrf  22420  cnnei  22442  cnrest2  22446  lmss  22458  lmres  22460  ist1-2  22507  ist1-3  22509  isreg2  22537  cmpfi  22568  bwth  22570  1stccn  22623  subislly  22641  kgencn  22716  ptclsg  22775  ptcnplem  22781  xkococnlem  22819  xkoinjcn  22847  tgqtop  22872  qtopcn  22874  fbflim  23136  flimrest  23143  flfnei  23151  isflf  23153  cnflf  23162  fclsopn  23174  fclsbas  23181  fclsrest  23184  isfcf  23194  cnfcf  23202  ptcmplem3  23214  tmdgsum2  23256  eltsms  23293  tsmsgsum  23299  tsmssubm  23303  tsmsf1o  23305  utopsnneiplem  23408  ismet2  23495  prdsxmetlem  23530  elmopn2  23607  prdsbl  23656  metss  23673  metrest  23689  metcnp  23706  metcnp2  23707  metcn  23708  metucn  23736  nrginvrcn  23865  metdsge  24021  divcn  24040  elcncf2  24062  mulc1cncf  24077  cncfmet  24081  evth2  24132  lmmbr2  24432  lmmbrf  24435  iscfil2  24439  cfil3i  24442  iscau2  24450  iscau4  24452  iscauf  24453  caucfil  24456  iscmet3lem3  24463  cfilres  24469  causs  24471  lmclim  24476  rrxmet  24581  evthicc2  24633  cniccbdd  24634  ovolfioo  24640  ovolficc  24641  ismbl2  24700  mbfsup  24837  mbfinf  24838  mbflimsup  24839  0plef  24845  mbfi1flim  24897  xrge0f  24905  itg2mulclem  24920  itgeqa  24987  ellimc2  25050  ellimc3  25052  limcflf  25054  cnlimc  25061  dvferm1  25158  dvferm2  25160  rolle  25163  dvivthlem1  25181  ftc1lem6  25214  itgsubst  25222  mdegle0  25251  deg1leb  25269  plydivex  25466  ulm2  25553  ulmcaulem  25562  ulmcau  25563  ulmdvlem3  25570  abelthlem9  25608  abelth  25609  rlimcnp  26124  ftalem3  26233  issqf  26294  sqf11  26297  dvdsmulf1o  26352  dchrelbas4  26400  dchrinv  26418  2sqlem6  26580  chpo1ubb  26638  dchrmusumlema  26650  dchrisum0lema  26671  ostth3  26795  tgcgr4  26901  eqeelen  27281  brbtwn2  27282  colinearalg  27287  axcgrid  27293  axsegconlem1  27294  ax5seglem4  27309  ax5seglem5  27310  axbtwnid  27316  axpasch  27318  axeuclidlem  27339  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  axcontlem12  27352  elntg2  27362  isuvtx  27771  uvtx2vtx1edg  27774  uvtx2vtx1edgb  27775  iscplgrnb  27792  iscplgredg  27793  vdiscusgrb  27906  uhgrvd00  27910  upgriswlk  28017  wwlksnext  28267  clwwlkinwwlk  28413  clwwlkel  28419  clwwlkf  28420  clwwlkwwlksb  28427  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  clwwlknonex2lem2  28481  nmounbi  29147  blocnilem  29175  isph  29193  phoeqi  29228  h2hcau  29350  h2hlm  29351  hial2eq2  29478  hoeq1  30201  hoeq2  30202  adjsym  30204  cnvadj  30263  hhcno  30275  hhcnf  30276  adjvalval  30308  leop2  30495  leoptri  30507  mdbr2  30667  dmdbr2  30674  mddmd2  30680  cdj3lem3b  30811  infxrge0gelb  31098  toslublem  31259  tosglblem  31261  mgccnv  31286  submarchi  31449  isarchi3  31450  lindfpropd  31585  cmpcref  31809  lmdvg  31912  prodindf  32000  eulerpartlemd  32342  subfacp1lem3  33153  subfacp1lem5  33155  satfv1lem  33333  dfrdg2  33780  sltrec  34023  lrrecfr  34109  opnrebl  34518  poimirlem23  35809  broucube  35820  itg2gt0cn  35841  ftc1cnnc  35858  lmclim2  35925  caures  35927  sstotbnd2  35941  rrnmet  35996  rrncmslem  35999  isdrngo3  36126  isidlc  36182  cvrval2  37295  isat3  37328  iscvlat2N  37345  glbconN  37398  ltrneq  38170  cdlemefrs29clN  38420  cdlemefrs32fva  38421  cdleme32fva  38458  cdlemk33N  38930  cdlemk34  38931  cdlemkid3N  38954  cdlemkid4  38955  diaglbN  39076  dibglbN  39187  dihglbcpreN  39321  dihglblem6  39361  hdmap1eulem  39843  hdmap1eulemOLDN  39844  hdmapoc  39952  hlhilocv  39982  wepwsolem  40874  fnwe2lem2  40883  islnm2  40910  iscard5  41150  alephiso2  41172  clsk3nimkb  41657  ntrclsneine0  41682  ntrneineine0  41704  ntrneineine1  41705  ntrneicls00  41706  ntrneicls11  41707  ntrneiiso  41708  ntrneik2  41709  ntrneix2  41710  ntrneikb  41711  ntrneixb  41712  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  ntrneik4w  41717  ntrneik4  41718  caofcan  41948  infxrbnd2  42915  supminfxr  43011  evthiccabs  43041  ellimcabssub0  43165  climf  43170  clim2f  43184  clim2cf  43198  clim0cf  43202  limsupmnflem  43268  limsupre2lem  43272  limsupreuzmpt  43287  supcnvlimsup  43288  limsupge  43309  liminfreuzlem  43350  liminfltlem  43352  liminflimsupclim  43355  liminfpnfuz  43364  xlimpnfxnegmnf2  43406  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem80  43734  fourierdlem83  43737  fourierdlem87  43741  voliunsge0lem  44017  meaiuninclem  44025  meaiuninc3v  44029  hoidmv1lelem3  44138  hoidmvlelem4  44143  hoidmvlelem5  44144  issmflem  44272  cfsetsnfsetf  44563  cfsetsnfsetfo  44565  requad2  45086  islinindfis  45801  elbigolo1  45914  line2x  46111  itscnhlinecirc02p  46142  iscnrm3lem1  46238  ipolublem  46283  ipoglblem  46286  aacllem  46516