Theorem ralbidva 3183

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  ralbidv  3185  2ralbidva  3224  raleqbidva  3325  poinxp  5731  soinxp  5732  frinxp  5733  ordunisssuc  6471  fnmptfvd  7040  funimass3  7053  fnnfpeq0  7183  cocan1  7299  cocan2  7300  isores2  7341  isoini2  7347  ofrfvalg  7701  ofrfval2  7714  caofidlcan  7731  tfindsg2  7873  f1oweALT  7984  fnwe2lem3  8147  fnsuppres  8208  dfsmo2  8355  smores  8360  smores2  8362  dfrecs3  8380  naddunif  8703  ac6sfi  9275  fimaxg  9278  ordunifi  9281  isfinite2  9290  fipreima  9347  supisolem  9466  fiming  9492  infempty  9501  ordiso2  9509  ordtypelem7  9518  cantnf  9694  wemapwe  9698  rankval3b  9836  rankonidlem  9838  iscard  10056  acndom  10130  dfac12lem3  10224  kmlem2  10230  cflim2  10341  cfsmolem  10348  ttukeylem6  10592  alephreg  10667  suplem2pr  11138  axsup  11385  sup3  12274  infm3  12276  suprleub  12283  dfinfre  12298  infregelb  12301  ofsubeq0  12317  ofsubge0  12319  zextlt  12773  prime  12780  suprfinzcl  12813  indstr  13043  supxr2  13444  supxrbnd1  13451  supxrbnd2  13452  supxrleub  13456  supxrbnd  13458  infxrgelb  13466  fzshftral  13749  mptnn0fsupp  14140  swrdspsleq  14815  pfxeq  14845  clim  15661  rlim  15662  clim2  15671  clim2c  15672  clim0c  15674  ello1mpt  15688  lo1o1  15699  o1lo1  15704  climabs0  15752  o1compt  15754  rlimdiv  15813  geomulcvg  16045  mertenslem2  16054  mertens  16055  rpnnen2lem12  16393  sqrt2irr  16417  fprodfvdvdsd  16504  fproddvdsd  16505  dfgcd2  16719  isprm7  16884  pc11  17058  pcz  17059  1arith  17105  vdwlem8  17166  vdwlem11  17169  vdw  17172  ramval  17186  pwsle  17664  mrieqvd  17812  mreacs  17832  cidpropd  17884  ismon2  17909  monpropd  17912  isepi  17915  isepi2  17916  subsubc  18028  funcres2b  18072  funcpropd  18077  isfull2  18088  isfth2  18092  fucsect  18150  fucinv  18151  pospropd  18499  ipodrsfi  18713  tsrss  18763  grpidpropd  18842  mgmidpfod  18857  sgrppropd  18920  mndpropd  18951  smndex1mnd  19109  grppropd  19162  issubg4  19356  gass  19515  gsmsymgrfixlem1  19641  gsmsymgreqlem2  19645  gexdvds  19798  gexdvds2  19799  subgpgp  19811  sylow3lem6  19846  efgval2  19938  efgsp1  19951  dprdf11  20239  subgdmdprd  20250  rngpropd  20396  ringpropd  20519  isdrng5  21008  abvpropd  21092  lsspropd  21292  lbspropd  21374  isridlrng  21498  isridl  21545  phlpropd  21961  ishil2  22025  frlmplusgvalb  22075  frlmvscavalb  22076  frlmvplusgscavalb  22077  lindfmm  22133  islindf4  22144  islindf5  22145  assapropd  22179  psrbaglefi  22234  psrbagconf1o  22237  gsumbagdiaglem  22239  mplmonmul  22345  gsumply1eq  22627  scmatf1  22846  cpmatmcllem  23036  cpmatmcl  23037  decpmataa0  23086  decpmatmulsumfsupp  23091  pmatcollpw2lem  23095  pm2mpmhmlem1  23136  tgss2  23305  isclo  23405  neips  23431  opnnei  23438  isperf3  23471  ssidcn  23573  lmbrf  23578  cnnei  23600  cnrest2  23604  lmss  23616  lmres  23618  ist1-2  23665  ist1-3  23667  isreg2  23695  cmpfi  23726  bwth  23728  1stccn  23782  subislly  23800  kgencn  23875  ptclsg  23934  ptcnplem  23940  xkococnlem  23978  xkoinjcn  24006  tgqtop  24031  qtopcn  24033  fbflim  24295  flimrest  24302  flfnei  24310  isflf  24312  cnflf  24321  fclsopn  24333  fclsbas  24340  fclsrest  24343  isfcf  24353  cnfcf  24361  ptcmplem3  24373  tmdgsum2  24415  eltsms  24452  tsmsgsum  24458  tsmssubm  24462  tsmsf1o  24464  utopsnneiplem  24566  ismet2  24652  prdsxmetlem  24687  elmopn2  24764  prdsbl  24810  metss  24827  metrest  24843  metcnp  24860  metcnp2  24861  metcn  24862  metucn  24890  nrginvrcn  25011  metdsge  25169  divcn  25189  elcncf2  25211  mulc1cncf  25226  cncfmet  25230  evth2  25281  lmmbr2  25580  lmmbrf  25583  iscfil2  25587  cfil3i  25590  iscau2  25598  iscau4  25600  iscauf  25601  caucfil  25604  iscmet3lem3  25611  cfilres  25617  causs  25619  lmclim  25624  rrxmet  25729  evthicc2  25781  cniccbdd  25782  ovolfioo  25788  ovolficc  25789  ismbl2  25848  mbfsup  25985  mbfinf  25986  mbflimsup  25987  0plef  25993  mbfi1flim  26044  xrge0f  26052  itg2mulclem  26067  itgeqa  26134  ellimc2  26197  ellimc3  26199  limcflf  26201  cnlimc  26208  dvferm1  26305  dvferm2  26307  rolle  26310  dvivthlem1  26328  ftc1lem6  26361  itgsubst  26369  mdegle0  26395  deg1leb  26413  plydivex  26618  rnplynfin  26630  ulm2  26712  ulmcaulem  26721  ulmcau  26722  ulmdvlem3  26729  abelthlem9  26767  abelth  26768  rlimcnp  27293  ftalem3  27402  issqf  27463  sqf11  27466  mpodvdsmulf1o  27521  dvdsmulf1o  27523  dchrelbas4  27570  dchrinv  27588  2sqlem6  27750  chpo1ubb  27808  dchrmusumlema  27820  dchrisum0lema  27841  ostth3  27965  ltsrec  28187  lrrecfr  28329  addsuniflem  28387  addbday  28404  negsunif  28441  n0fincut  28741  bdayfinbndlem1  28853  elreno2  28881  tgcgr4  28994  eqeelen  29482  brbtwn2  29483  colinearalg  29488  axcgrid  29494  axsegconlem1  29495  ax5seglem4  29510  ax5seglem5  29511  axbtwnid  29517  axpasch  29519  axeuclidlem  29540  axcontlem2  29543  axcontlem4  29545  axcontlem7  29548  axcontlem12  29553  elntg2  29563  isuvtx  29976  uvtx2vtx1edg  29979  uvtx2vtx1edgb  29980  iscplgrnb  29997  iscplgredg  29998  vdiscusgrb  30111  uhgrvd00  30115  upgriswlk  30221  wwlksnext  30482  clwwlkinwwlk  30631  clwwlkel  30637  clwwlkf  30638  clwwlkwwlksb  30645  wwlksext2clwwlk  30648  wwlksubclwwlk  30649  clwwlknonex2lem2  30699  nmounbi  31378  blocnilem  31406  isph  31424  phoeqi  31459  h2hcau  31581  h2hlm  31582  hial2eq2  31709  hoeq1  32432  hoeq2  32433  adjsym  32435  cnvadj  32494  hhcno  32506  hhcnf  32507  adjvalval  32539  leop2  32726  leoptri  32738  mdbr2  32898  dmdbr2  32905  mddmd2  32911  cdj3lem3b  33042  infxrge0gelb  33358  prodindf  33429  toslublem  33533  tosglblem  33535  mgccnv  33560  cntrval2  33732  submarchi  33747  isarchi3  33748  lindfpropd  33937  opprlidlabs  34009  ply1moneq  34120  psrmonmul  34182  cmpcref  34482  lmdvg  34585  eulerpartlemd  34998  subfacp1lem3  35947  subfacp1lem5  35949  satfv1lem  36127  dfrdg2  36557  nadddilem2  36970  nadddilem4  36972  opnrebl  37108  poimirlem23  38562  broucube  38573  itg2gt0cn  38594  ftc1cnnc  38611  lmclim2  38693  caures  38695  sstotbnd2  38709  rrnmet  38764  rrncmslem  38767  isdrngo3  38894  isidlc  38950  cvrval2  40332  isat3  40365  iscvlat2N  40382  glbconN  40435  ltrneq  41207  cdlemefrs29clN  41457  cdlemefrs32fva  41458  cdleme32fva  41495  cdlemk33N  41967  cdlemk34  41968  cdlemkid3N  41991  cdlemkid4  41992  diaglbN  42113  dibglbN  42224  dihglbcpreN  42358  dihglblem6  42398  hdmap1eulem  42880  hdmap1eulemOLDN  42881  hdmapoc  42989  hlhilocv  43015  primrootsunit1  43148  sn-sup3d  43557  fimgmcyc  43599  wepwsolem  44049  islnm2  44080  onmaxnelsup  44225  onsupnmax  44230  onsupuni  44231  onsupmaxb  44241  onsupeqnmax  44249  iscard5  44537  alephiso2  44559  clsk3nimkb  45040  ntrclsneine0  45065  ntrneineine0  45087  ntrneineine1  45088  ntrneicls00  45089  ntrneicls11  45090  ntrneiiso  45091  ntrneik2  45092  ntrneix2  45093  ntrneikb  45094  ntrneixb  45095  ntrneik3  45096  ntrneix3  45097  ntrneik13  45098  ntrneix13  45099  ntrneik4w  45100  ntrneik4  45101  caofcan  45307  modelac8prim  45982  infxrbnd2  46380  supminfxr  46474  rexanuz2nf  46502  evthiccabs  46508  ellimcabssub0  46629  climf  46634  clim2f  46646  clim2cf  46660  clim0cf  46664  limsupmnflem  46730  limsupre2lem  46734  limsupreuzmpt  46749  supcnvlimsup  46750  limsupge  46771  liminfreuzlem  46812  liminfltlem  46814  liminflimsupclim  46817  liminfpnfuz  46826  xlimpnfxnegmnf2  46868  fourierdlem70  47186  fourierdlem71  47187  fourierdlem73  47189  fourierdlem80  47196  fourierdlem83  47199  fourierdlem87  47203  voliunsge0lem  47482  meaiuninclem  47490  meaiuninc3v  47494  hoidmv1lelem3  47603  hoidmvlelem4  47608  hoidmvlelem5  47609  issmflem  47737  chnerlem1  47892  cfsetsnfsetf  48128  cfsetsnfsetfo  48130  nprmmul1  48609  requad2  48721  isubgrgrim  49027  grlicref  49110  islinindfis  49561  elbigolo1  49669  line2x  49866  itscnhlinecirc02p  49897  iscnrm3lem1  50042  ipolublem  50094  ipoglblem  50097  oppcup  50315  uptrlem3  50320  initopropd  50351  termopropd  50352  isinito2lem  50606  termc2  50626  lanup  50749  ranup  50750  aacllem  50939