Theorem ralbidva 3154

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralbidv  3156  2ralbidva  3197  raleqbidva  3302  poinxp  5712  soinxp  5713  frinxp  5714  ordunisssuc  6428  fnmptfvd  6995  funimass3  7008  fnnfpeq0  7134  cocan1  7248  cocan2  7249  isores2  7290  isoini2  7296  ofrfvalg  7641  ofrfval2  7654  caofidlcan  7671  tfindsg2  7818  f1oweALT  7930  fnsuppres  8147  dfsmo2  8293  smores  8298  smores2  8300  dfrecs3  8318  naddunif  8634  ac6sfi  9207  fimaxg  9210  ordunifi  9213  isfinite2  9221  fipreima  9285  supisolem  9401  fiming  9427  infempty  9436  ordiso2  9444  ordtypelem7  9453  cantnf  9624  wemapwe  9628  rankval3b  9757  rankonidlem  9759  iscard  9906  acndom  9982  dfac12lem3  10077  kmlem2  10083  cflim2  10194  cfsmolem  10201  ttukeylem6  10445  alephreg  10513  suplem2pr  10984  axsup  11227  sup3  12118  infm3  12120  suprleub  12127  dfinfre  12142  infregelb  12145  ofsubeq0  12161  ofsubge0  12163  zextlt  12586  prime  12593  suprfinzcl  12626  indstr  12853  supxr2  13252  supxrbnd1  13259  supxrbnd2  13260  supxrleub  13264  supxrbnd  13266  infxrgelb  13274  fzshftral  13554  mptnn0fsupp  13940  swrdspsleq  14608  pfxeq  14638  clim  15437  rlim  15438  clim2  15447  clim2c  15448  clim0c  15450  ello1mpt  15464  lo1o1  15475  o1lo1  15480  climabs0  15528  o1compt  15530  rlimdiv  15589  geomulcvg  15819  mertenslem2  15828  mertens  15829  rpnnen2lem12  16170  sqrt2irr  16194  fprodfvdvdsd  16281  fproddvdsd  16282  dfgcd2  16493  isprm7  16655  pc11  16828  pcz  16829  1arith  16875  vdwlem8  16936  vdwlem11  16939  vdw  16942  ramval  16956  pwsle  17432  mrieqvd  17580  mreacs  17600  cidpropd  17652  ismon2  17677  monpropd  17680  isepi  17683  isepi2  17684  subsubc  17796  funcres2b  17840  funcpropd  17845  isfull2  17856  isfth2  17860  fucsect  17918  fucinv  17919  pospropd  18267  ipodrsfi  18481  tsrss  18531  grpidpropd  18572  sgrppropd  18641  mndpropd  18669  smndex1mnd  18820  grppropd  18866  issubg4  19060  gass  19216  gsmsymgrfixlem1  19342  gsmsymgreqlem2  19346  gexdvds  19499  gexdvds2  19500  subgpgp  19512  sylow3lem6  19547  efgval2  19639  efgsp1  19652  dprdf11  19940  subgdmdprd  19951  rngpropd  20095  ringpropd  20209  abvpropd  20756  lsspropd  20957  lbspropd  21039  isridlrng  21162  isridl  21195  phlpropd  21598  ishil2  21662  frlmplusgvalb  21712  frlmvscavalb  21713  frlmvplusgscavalb  21714  lindfmm  21770  islindf4  21781  islindf5  21782  assapropd  21815  psrbaglefi  21869  psrbagconf1o  21872  gsumbagdiaglem  21873  mplmonmul  21977  gsumply1eq  22230  scmatf1  22452  cpmatmcllem  22639  cpmatmcl  22640  decpmataa0  22689  decpmatmulsumfsupp  22694  pmatcollpw2lem  22698  pm2mpmhmlem1  22739  tgss2  22908  isclo  23008  neips  23034  opnnei  23041  isperf3  23074  ssidcn  23176  lmbrf  23181  cnnei  23203  cnrest2  23207  lmss  23219  lmres  23221  ist1-2  23268  ist1-3  23270  isreg2  23298  cmpfi  23329  bwth  23331  1stccn  23384  subislly  23402  kgencn  23477  ptclsg  23536  ptcnplem  23542  xkococnlem  23580  xkoinjcn  23608  tgqtop  23633  qtopcn  23635  fbflim  23897  flimrest  23904  flfnei  23912  isflf  23914  cnflf  23923  fclsopn  23935  fclsbas  23942  fclsrest  23945  isfcf  23955  cnfcf  23963  ptcmplem3  23975  tmdgsum2  24017  eltsms  24054  tsmsgsum  24060  tsmssubm  24064  tsmsf1o  24066  utopsnneiplem  24169  ismet2  24255  prdsxmetlem  24290  elmopn2  24367  prdsbl  24413  metss  24430  metrest  24446  metcnp  24463  metcnp2  24464  metcn  24465  metucn  24493  nrginvrcn  24614  metdsge  24772  divcnOLD  24791  divcn  24793  elcncf2  24817  mulc1cncf  24832  cncfmet  24836  evth2  24893  lmmbr2  25193  lmmbrf  25196  iscfil2  25200  cfil3i  25203  iscau2  25211  iscau4  25213  iscauf  25214  caucfil  25217  iscmet3lem3  25224  cfilres  25230  causs  25232  lmclim  25237  rrxmet  25342  evthicc2  25395  cniccbdd  25396  ovolfioo  25402  ovolficc  25403  ismbl2  25462  mbfsup  25599  mbfinf  25600  mbflimsup  25601  0plef  25607  mbfi1flim  25658  xrge0f  25666  itg2mulclem  25681  itgeqa  25749  ellimc2  25812  ellimc3  25814  limcflf  25816  cnlimc  25823  dvferm1  25923  dvferm2  25925  rolle  25928  dvivthlem1  25947  ftc1lem6  25982  itgsubst  25990  mdegle0  26016  deg1leb  26034  plydivex  26239  ulm2  26328  ulmcaulem  26337  ulmcau  26338  ulmdvlem3  26345  abelthlem9  26384  abelth  26385  rlimcnp  26909  ftalem3  27019  issqf  27080  sqf11  27083  mpodvdsmulf1o  27138  dvdsmulf1o  27140  dchrelbas4  27188  dchrinv  27206  2sqlem6  27368  chpo1ubb  27426  dchrmusumlema  27438  dchrisum0lema  27459  ostth3  27583  sltrec  27768  lrrecfr  27891  addsuniflem  27949  addsbday  27965  negsunif  28002  n0sfincut  28287  tgcgr4  28512  eqeelen  28885  brbtwn2  28886  colinearalg  28891  axcgrid  28897  axsegconlem1  28898  ax5seglem4  28913  ax5seglem5  28914  axbtwnid  28920  axpasch  28922  axeuclidlem  28943  axcontlem2  28946  axcontlem4  28948  axcontlem7  28951  axcontlem12  28956  elntg2  28966  isuvtx  29376  uvtx2vtx1edg  29379  uvtx2vtx1edgb  29380  iscplgrnb  29397  iscplgredg  29398  vdiscusgrb  29512  uhgrvd00  29516  upgriswlk  29622  wwlksnext  29874  clwwlkinwwlk  30020  clwwlkel  30026  clwwlkf  30027  clwwlkwwlksb  30034  wwlksext2clwwlk  30037  wwlksubclwwlk  30038  clwwlknonex2lem2  30088  nmounbi  30756  blocnilem  30784  isph  30802  phoeqi  30837  h2hcau  30959  h2hlm  30960  hial2eq2  31087  hoeq1  31810  hoeq2  31811  adjsym  31813  cnvadj  31872  hhcno  31884  hhcnf  31885  adjvalval  31917  leop2  32104  leoptri  32116  mdbr2  32276  dmdbr2  32283  mddmd2  32289  cdj3lem3b  32420  infxrge0gelb  32740  prodindf  32837  toslublem  32945  tosglblem  32947  mgccnv  32972  cntrval2  33144  submarchi  33156  isarchi3  33157  lindfpropd  33347  opprlidlabs  33450  ply1moneq  33549  cmpcref  33834  lmdvg  33937  eulerpartlemd  34351  subfacp1lem3  35163  subfacp1lem5  35165  satfv1lem  35343  dfrdg2  35777  opnrebl  36302  poimirlem23  37631  broucube  37642  itg2gt0cn  37663  ftc1cnnc  37680  lmclim2  37746  caures  37748  sstotbnd2  37762  rrnmet  37817  rrncmslem  37820  isdrngo3  37947  isidlc  38003  cvrval2  39261  isat3  39294  iscvlat2N  39311  glbconN  39364  glbconNOLD  39365  ltrneq  40137  cdlemefrs29clN  40387  cdlemefrs32fva  40388  cdleme32fva  40425  cdlemk33N  40897  cdlemk34  40898  cdlemkid3N  40921  cdlemkid4  40922  diaglbN  41043  dibglbN  41154  dihglbcpreN  41288  dihglblem6  41328  hdmap1eulem  41810  hdmap1eulemOLDN  41811  hdmapoc  41919  hlhilocv  41945  primrootsunit1  42079  sn-sup3d  42474  fimgmcyc  42516  wepwsolem  43025  fnwe2lem2  43034  islnm2  43061  onmaxnelsup  43206  onsupnmax  43211  onsupuni  43212  onsupmaxb  43222  onsupeqnmax  43230  iscard5  43519  alephiso2  43541  clsk3nimkb  44023  ntrclsneine0  44048  ntrneineine0  44070  ntrneineine1  44071  ntrneicls00  44072  ntrneicls11  44073  ntrneiiso  44074  ntrneik2  44075  ntrneix2  44076  ntrneikb  44077  ntrneixb  44078  ntrneik3  44079  ntrneix3  44080  ntrneik13  44081  ntrneix13  44082  ntrneik4w  44083  ntrneik4  44084  caofcan  44306  modelac8prim  44976  infxrbnd2  45359  supminfxr  45454  rexanuz2nf  45482  evthiccabs  45488  ellimcabssub0  45609  climf  45614  clim2f  45628  clim2cf  45642  clim0cf  45646  limsupmnflem  45712  limsupre2lem  45716  limsupreuzmpt  45731  supcnvlimsup  45732  limsupge  45753  liminfreuzlem  45794  liminfltlem  45796  liminflimsupclim  45799  liminfpnfuz  45808  xlimpnfxnegmnf2  45850  fourierdlem70  46168  fourierdlem71  46169  fourierdlem73  46171  fourierdlem80  46178  fourierdlem83  46181  fourierdlem87  46185  voliunsge0lem  46464  meaiuninclem  46472  meaiuninc3v  46476  hoidmv1lelem3  46585  hoidmvlelem4  46590  hoidmvlelem5  46591  issmflem  46719  cfsetsnfsetf  47053  cfsetsnfsetfo  47055  requad2  47618  isubgrgrim  47923  grlicref  47998  islinindfis  48432  elbigolo1  48540  line2x  48737  itscnhlinecirc02p  48768  iscnrm3lem1  48916  ipolublem  48968  ipoglblem  48971  oppcup  49190  uptrlem3  49195  initopropd  49226  termopropd  49227  isinito2lem  49481  termc2  49501  lanup  49624  ranup  49625  aacllem  49784