Theorem ralbidva 3158

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 804	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜒)))
3	2	ralbidv2 3156	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  ralbidv  3160  2ralbidva  3199  raleqbidva  3301  poinxp  5712  soinxp  5713  frinxp  5714  ordunisssuc  6431  fnmptfvd  6993  funimass3  7006  fnnfpeq0  7133  cocan1  7246  cocan2  7247  isores2  7288  isoini2  7294  ofrfvalg  7639  ofrfval2  7652  caofidlcan  7669  tfindsg2  7813  f1oweALT  7925  fnsuppres  8141  dfsmo2  8287  smores  8292  smores2  8294  dfrecs3  8312  naddunif  8629  ac6sfi  9194  fimaxg  9197  ordunifi  9200  isfinite2  9208  fipreima  9268  supisolem  9387  fiming  9413  infempty  9422  ordiso2  9430  ordtypelem7  9439  cantnf  9614  wemapwe  9618  rankval3b  9750  rankonidlem  9752  iscard  9899  acndom  9973  dfac12lem3  10068  kmlem2  10074  cflim2  10185  cfsmolem  10192  ttukeylem6  10436  alephreg  10505  suplem2pr  10976  axsup  11221  sup3  12113  infm3  12115  suprleub  12122  dfinfre  12137  infregelb  12140  ofsubeq0  12156  ofsubge0  12158  zextlt  12603  prime  12610  suprfinzcl  12643  indstr  12866  supxr2  13266  supxrbnd1  13273  supxrbnd2  13274  supxrleub  13278  supxrbnd  13280  infxrgelb  13288  fzshftral  13569  mptnn0fsupp  13959  swrdspsleq  14628  pfxeq  14658  clim  15456  rlim  15457  clim2  15466  clim2c  15467  clim0c  15469  ello1mpt  15483  lo1o1  15494  o1lo1  15499  climabs0  15547  o1compt  15549  rlimdiv  15608  geomulcvg  15841  mertenslem2  15850  mertens  15851  rpnnen2lem12  16192  sqrt2irr  16216  fprodfvdvdsd  16303  fproddvdsd  16304  dfgcd2  16515  isprm7  16678  pc11  16851  pcz  16852  1arith  16898  vdwlem8  16959  vdwlem11  16962  vdw  16965  ramval  16979  pwsle  17456  mrieqvd  17604  mreacs  17624  cidpropd  17676  ismon2  17701  monpropd  17704  isepi  17707  isepi2  17708  subsubc  17820  funcres2b  17864  funcpropd  17869  isfull2  17880  isfth2  17884  fucsect  17942  fucinv  17943  pospropd  18291  ipodrsfi  18505  tsrss  18555  grpidpropd  18630  sgrppropd  18699  mndpropd  18727  smndex1mnd  18881  grppropd  18927  issubg4  19121  gass  19276  gsmsymgrfixlem1  19402  gsmsymgreqlem2  19406  gexdvds  19559  gexdvds2  19560  subgpgp  19572  sylow3lem6  19607  efgval2  19699  efgsp1  19712  dprdf11  20000  subgdmdprd  20011  rngpropd  20155  ringpropd  20269  abvpropd  20812  lsspropd  21012  lbspropd  21094  isridlrng  21217  isridl  21250  phlpropd  21635  ishil2  21699  frlmplusgvalb  21749  frlmvscavalb  21750  frlmvplusgscavalb  21751  lindfmm  21807  islindf4  21818  islindf5  21819  assapropd  21851  psrbaglefi  21906  psrbagconf1o  21909  gsumbagdiaglem  21910  mplmonmul  22014  gsumply1eq  22274  scmatf1  22496  cpmatmcllem  22683  cpmatmcl  22684  decpmataa0  22733  decpmatmulsumfsupp  22738  pmatcollpw2lem  22742  pm2mpmhmlem1  22783  tgss2  22952  isclo  23052  neips  23078  opnnei  23085  isperf3  23118  ssidcn  23220  lmbrf  23225  cnnei  23247  cnrest2  23251  lmss  23263  lmres  23265  ist1-2  23312  ist1-3  23314  isreg2  23342  cmpfi  23373  bwth  23375  1stccn  23428  subislly  23446  kgencn  23521  ptclsg  23580  ptcnplem  23586  xkococnlem  23624  xkoinjcn  23652  tgqtop  23677  qtopcn  23679  fbflim  23941  flimrest  23948  flfnei  23956  isflf  23958  cnflf  23967  fclsopn  23979  fclsbas  23986  fclsrest  23989  isfcf  23999  cnfcf  24007  ptcmplem3  24019  tmdgsum2  24061  eltsms  24098  tsmsgsum  24104  tsmssubm  24108  tsmsf1o  24110  utopsnneiplem  24212  ismet2  24298  prdsxmetlem  24333  elmopn2  24410  prdsbl  24456  metss  24473  metrest  24489  metcnp  24506  metcnp2  24507  metcn  24508  metucn  24536  nrginvrcn  24657  metdsge  24815  divcn  24835  elcncf2  24857  mulc1cncf  24872  cncfmet  24876  evth2  24927  lmmbr2  25226  lmmbrf  25229  iscfil2  25233  cfil3i  25236  iscau2  25244  iscau4  25246  iscauf  25247  caucfil  25250  iscmet3lem3  25257  cfilres  25263  causs  25265  lmclim  25270  rrxmet  25375  evthicc2  25427  cniccbdd  25428  ovolfioo  25434  ovolficc  25435  ismbl2  25494  mbfsup  25631  mbfinf  25632  mbflimsup  25633  0plef  25639  mbfi1flim  25690  xrge0f  25698  itg2mulclem  25713  itgeqa  25781  ellimc2  25844  ellimc3  25846  limcflf  25848  cnlimc  25855  dvferm1  25952  dvferm2  25954  rolle  25957  dvivthlem1  25975  ftc1lem6  26008  itgsubst  26016  mdegle0  26042  deg1leb  26060  plydivex  26263  ulm2  26350  ulmcaulem  26359  ulmcau  26360  ulmdvlem3  26367  abelthlem9  26405  abelth  26406  rlimcnp  26929  ftalem3  27038  issqf  27099  sqf11  27102  mpodvdsmulf1o  27157  dvdsmulf1o  27159  dchrelbas4  27206  dchrinv  27224  2sqlem6  27386  chpo1ubb  27444  dchrmusumlema  27456  dchrisum0lema  27477  ostth3  27601  ltsrec  27793  lrrecfr  27935  addsuniflem  27993  addbday  28010  negsunif  28047  n0fincut  28347  bdayfinbndlem1  28459  elreno2  28487  tgcgr4  28599  eqeelen  28973  brbtwn2  28974  colinearalg  28979  axcgrid  28985  axsegconlem1  28986  ax5seglem4  29001  ax5seglem5  29002  axbtwnid  29008  axpasch  29010  axeuclidlem  29031  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem12  29044  elntg2  29054  isuvtx  29464  uvtx2vtx1edg  29467  uvtx2vtx1edgb  29468  iscplgrnb  29485  iscplgredg  29486  vdiscusgrb  29599  uhgrvd00  29603  upgriswlk  29709  wwlksnext  29961  clwwlkinwwlk  30110  clwwlkel  30116  clwwlkf  30117  clwwlkwwlksb  30124  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  clwwlknonex2lem2  30178  nmounbi  30847  blocnilem  30875  isph  30893  phoeqi  30928  h2hcau  31050  h2hlm  31051  hial2eq2  31178  hoeq1  31901  hoeq2  31902  adjsym  31904  cnvadj  31963  hhcno  31975  hhcnf  31976  adjvalval  32008  leop2  32195  leoptri  32207  mdbr2  32367  dmdbr2  32374  mddmd2  32380  cdj3lem3b  32511  infxrge0gelb  32839  prodindf  32922  toslublem  33032  tosglblem  33034  mgccnv  33059  cntrval2  33232  submarchi  33247  isarchi3  33248  lindfpropd  33442  opprlidlabs  33545  ply1moneq  33648  psrmonmul  33694  cmpcref  33994  lmdvg  34097  eulerpartlemd  34510  subfacp1lem3  35364  subfacp1lem5  35366  satfv1lem  35544  dfrdg2  35975  opnrebl  36502  poimirlem23  37964  broucube  37975  itg2gt0cn  37996  ftc1cnnc  38013  lmclim2  38079  caures  38081  sstotbnd2  38095  rrnmet  38150  rrncmslem  38153  isdrngo3  38280  isidlc  38336  cvrval2  39720  isat3  39753  iscvlat2N  39770  glbconN  39823  ltrneq  40595  cdlemefrs29clN  40845  cdlemefrs32fva  40846  cdleme32fva  40883  cdlemk33N  41355  cdlemk34  41356  cdlemkid3N  41379  cdlemkid4  41380  diaglbN  41501  dibglbN  41612  dihglbcpreN  41746  dihglblem6  41786  hdmap1eulem  42268  hdmap1eulemOLDN  42269  hdmapoc  42377  hlhilocv  42403  primrootsunit1  42536  sn-sup3d  42937  fimgmcyc  42979  wepwsolem  43470  fnwe2lem2  43479  islnm2  43506  onmaxnelsup  43651  onsupnmax  43656  onsupuni  43657  onsupmaxb  43667  onsupeqnmax  43675  iscard5  43963  alephiso2  43985  clsk3nimkb  44467  ntrclsneine0  44492  ntrneineine0  44514  ntrneineine1  44515  ntrneicls00  44516  ntrneicls11  44517  ntrneiiso  44518  ntrneik2  44519  ntrneix2  44520  ntrneikb  44521  ntrneixb  44522  ntrneik3  44523  ntrneix3  44524  ntrneik13  44525  ntrneix13  44526  ntrneik4w  44527  ntrneik4  44528  caofcan  44750  modelac8prim  45419  infxrbnd2  45798  supminfxr  45892  rexanuz2nf  45920  evthiccabs  45926  ellimcabssub0  46047  climf  46052  clim2f  46064  clim2cf  46078  clim0cf  46082  limsupmnflem  46148  limsupre2lem  46152  limsupreuzmpt  46167  supcnvlimsup  46168  limsupge  46189  liminfreuzlem  46230  liminfltlem  46232  liminflimsupclim  46235  liminfpnfuz  46244  xlimpnfxnegmnf2  46286  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem80  46614  fourierdlem83  46617  fourierdlem87  46621  voliunsge0lem  46900  meaiuninclem  46908  meaiuninc3v  46912  hoidmv1lelem3  47021  hoidmvlelem4  47026  hoidmvlelem5  47027  issmflem  47155  chnerlem1  47312  cfsetsnfsetf  47506  cfsetsnfsetfo  47508  nprmmul1  47987  requad2  48099  isubgrgrim  48405  grlicref  48488  islinindfis  48925  elbigolo1  49033  line2x  49230  itscnhlinecirc02p  49261  iscnrm3lem1  49409  ipolublem  49461  ipoglblem  49464  oppcup  49682  uptrlem3  49687  initopropd  49718  termopropd  49719  isinito2lem  49973  termc2  49993  lanup  50116  ranup  50117  aacllem  50276