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 3052

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 3053

This theorem is referenced by:  ralbidv  3160  2ralbidva  3199  raleqbidva  3303  poinxp  5706  soinxp  5707  frinxp  5708  ordunisssuc  6426  fnmptfvd  6988  funimass3  7001  fnnfpeq0  7126  cocan1  7239  cocan2  7240  isores2  7281  isoini2  7287  ofrfvalg  7632  ofrfval2  7645  caofidlcan  7662  tfindsg2  7806  f1oweALT  7918  fnsuppres  8135  dfsmo2  8281  smores  8286  smores2  8288  dfrecs3  8306  naddunif  8623  ac6sfi  9188  fimaxg  9191  ordunifi  9194  isfinite2  9202  fipreima  9262  supisolem  9381  fiming  9407  infempty  9416  ordiso2  9424  ordtypelem7  9433  cantnf  9606  wemapwe  9610  rankval3b  9742  rankonidlem  9744  iscard  9891  acndom  9965  dfac12lem3  10060  kmlem2  10066  cflim2  10177  cfsmolem  10184  ttukeylem6  10428  alephreg  10497  suplem2pr  10968  axsup  11212  sup3  12103  infm3  12105  suprleub  12112  dfinfre  12127  infregelb  12130  ofsubeq0  12146  ofsubge0  12148  zextlt  12570  prime  12577  suprfinzcl  12610  indstr  12833  supxr2  13233  supxrbnd1  13240  supxrbnd2  13241  supxrleub  13245  supxrbnd  13247  infxrgelb  13255  fzshftral  13535  mptnn0fsupp  13924  swrdspsleq  14593  pfxeq  14623  clim  15421  rlim  15422  clim2  15431  clim2c  15432  clim0c  15434  ello1mpt  15448  lo1o1  15459  o1lo1  15464  climabs0  15512  o1compt  15514  rlimdiv  15573  geomulcvg  15803  mertenslem2  15812  mertens  15813  rpnnen2lem12  16154  sqrt2irr  16178  fprodfvdvdsd  16265  fproddvdsd  16266  dfgcd2  16477  isprm7  16639  pc11  16812  pcz  16813  1arith  16859  vdwlem8  16920  vdwlem11  16923  vdw  16926  ramval  16940  pwsle  17417  mrieqvd  17565  mreacs  17585  cidpropd  17637  ismon2  17662  monpropd  17665  isepi  17668  isepi2  17669  subsubc  17781  funcres2b  17825  funcpropd  17830  isfull2  17841  isfth2  17845  fucsect  17903  fucinv  17904  pospropd  18252  ipodrsfi  18466  tsrss  18516  grpidpropd  18591  sgrppropd  18660  mndpropd  18688  smndex1mnd  18839  grppropd  18885  issubg4  19079  gass  19234  gsmsymgrfixlem1  19360  gsmsymgreqlem2  19364  gexdvds  19517  gexdvds2  19518  subgpgp  19530  sylow3lem6  19565  efgval2  19657  efgsp1  19670  dprdf11  19958  subgdmdprd  19969  rngpropd  20113  ringpropd  20227  abvpropd  20772  lsspropd  20973  lbspropd  21055  isridlrng  21178  isridl  21211  phlpropd  21614  ishil2  21678  frlmplusgvalb  21728  frlmvscavalb  21729  frlmvplusgscavalb  21730  lindfmm  21786  islindf4  21797  islindf5  21798  assapropd  21831  psrbaglefi  21886  psrbagconf1o  21889  gsumbagdiaglem  21890  mplmonmul  21995  gsumply1eq  22257  scmatf1  22479  cpmatmcllem  22666  cpmatmcl  22667  decpmataa0  22716  decpmatmulsumfsupp  22721  pmatcollpw2lem  22725  pm2mpmhmlem1  22766  tgss2  22935  isclo  23035  neips  23061  opnnei  23068  isperf3  23101  ssidcn  23203  lmbrf  23208  cnnei  23230  cnrest2  23234  lmss  23246  lmres  23248  ist1-2  23295  ist1-3  23297  isreg2  23325  cmpfi  23356  bwth  23358  1stccn  23411  subislly  23429  kgencn  23504  ptclsg  23563  ptcnplem  23569  xkococnlem  23607  xkoinjcn  23635  tgqtop  23660  qtopcn  23662  fbflim  23924  flimrest  23931  flfnei  23939  isflf  23941  cnflf  23950  fclsopn  23962  fclsbas  23969  fclsrest  23972  isfcf  23982  cnfcf  23990  ptcmplem3  24002  tmdgsum2  24044  eltsms  24081  tsmsgsum  24087  tsmssubm  24091  tsmsf1o  24093  utopsnneiplem  24195  ismet2  24281  prdsxmetlem  24316  elmopn2  24393  prdsbl  24439  metss  24456  metrest  24472  metcnp  24489  metcnp2  24490  metcn  24491  metucn  24519  nrginvrcn  24640  metdsge  24798  divcnOLD  24817  divcn  24819  elcncf2  24843  mulc1cncf  24858  cncfmet  24862  evth2  24919  lmmbr2  25219  lmmbrf  25222  iscfil2  25226  cfil3i  25229  iscau2  25237  iscau4  25239  iscauf  25240  caucfil  25243  iscmet3lem3  25250  cfilres  25256  causs  25258  lmclim  25263  rrxmet  25368  evthicc2  25421  cniccbdd  25422  ovolfioo  25428  ovolficc  25429  ismbl2  25488  mbfsup  25625  mbfinf  25626  mbflimsup  25627  0plef  25633  mbfi1flim  25684  xrge0f  25692  itg2mulclem  25707  itgeqa  25775  ellimc2  25838  ellimc3  25840  limcflf  25842  cnlimc  25849  dvferm1  25949  dvferm2  25951  rolle  25954  dvivthlem1  25973  ftc1lem6  26008  itgsubst  26016  mdegle0  26042  deg1leb  26060  plydivex  26265  ulm2  26354  ulmcaulem  26363  ulmcau  26364  ulmdvlem3  26371  abelthlem9  26410  abelth  26411  rlimcnp  26935  ftalem3  27045  issqf  27106  sqf11  27109  mpodvdsmulf1o  27164  dvdsmulf1o  27166  dchrelbas4  27214  dchrinv  27232  2sqlem6  27394  chpo1ubb  27452  dchrmusumlema  27464  dchrisum0lema  27485  ostth3  27609  ltsrec  27801  lrrecfr  27943  addsuniflem  28001  addbday  28018  negsunif  28055  n0fincut  28355  bdayfinbndlem1  28467  elreno2  28495  tgcgr4  28607  eqeelen  28981  brbtwn2  28982  colinearalg  28987  axcgrid  28993  axsegconlem1  28994  ax5seglem4  29009  ax5seglem5  29010  axbtwnid  29016  axpasch  29018  axeuclidlem  29039  axcontlem2  29042  axcontlem4  29044  axcontlem7  29047  axcontlem12  29052  elntg2  29062  isuvtx  29472  uvtx2vtx1edg  29475  uvtx2vtx1edgb  29476  iscplgrnb  29493  iscplgredg  29494  vdiscusgrb  29608  uhgrvd00  29612  upgriswlk  29718  wwlksnext  29970  clwwlkinwwlk  30119  clwwlkel  30125  clwwlkf  30126  clwwlkwwlksb  30133  wwlksext2clwwlk  30136  wwlksubclwwlk  30137  clwwlknonex2lem2  30187  nmounbi  30855  blocnilem  30883  isph  30901  phoeqi  30936  h2hcau  31058  h2hlm  31059  hial2eq2  31186  hoeq1  31909  hoeq2  31910  adjsym  31912  cnvadj  31971  hhcno  31983  hhcnf  31984  adjvalval  32016  leop2  32203  leoptri  32215  mdbr2  32375  dmdbr2  32382  mddmd2  32388  cdj3lem3b  32519  infxrge0gelb  32848  prodindf  32946  toslublem  33056  tosglblem  33058  mgccnv  33083  cntrval2  33255  submarchi  33270  isarchi3  33271  lindfpropd  33465  opprlidlabs  33568  ply1moneq  33671  cmpcref  34009  lmdvg  34112  eulerpartlemd  34525  subfacp1lem3  35378  subfacp1lem5  35380  satfv1lem  35558  dfrdg2  35989  opnrebl  36516  poimirlem23  37846  broucube  37857  itg2gt0cn  37878  ftc1cnnc  37895  lmclim2  37961  caures  37963  sstotbnd2  37977  rrnmet  38032  rrncmslem  38035  isdrngo3  38162  isidlc  38218  cvrval2  39602  isat3  39635  iscvlat2N  39652  glbconN  39705  ltrneq  40477  cdlemefrs29clN  40727  cdlemefrs32fva  40728  cdleme32fva  40765  cdlemk33N  41237  cdlemk34  41238  cdlemkid3N  41261  cdlemkid4  41262  diaglbN  41383  dibglbN  41494  dihglbcpreN  41628  dihglblem6  41668  hdmap1eulem  42150  hdmap1eulemOLDN  42151  hdmapoc  42259  hlhilocv  42285  primrootsunit1  42419  sn-sup3d  42814  fimgmcyc  42856  wepwsolem  43351  fnwe2lem2  43360  islnm2  43387  onmaxnelsup  43532  onsupnmax  43537  onsupuni  43538  onsupmaxb  43548  onsupeqnmax  43556  iscard5  43844  alephiso2  43866  clsk3nimkb  44348  ntrclsneine0  44373  ntrneineine0  44395  ntrneineine1  44396  ntrneicls00  44397  ntrneicls11  44398  ntrneiiso  44399  ntrneik2  44400  ntrneix2  44401  ntrneikb  44402  ntrneixb  44403  ntrneik3  44404  ntrneix3  44405  ntrneik13  44406  ntrneix13  44407  ntrneik4w  44408  ntrneik4  44409  caofcan  44631  modelac8prim  45300  infxrbnd2  45680  supminfxr  45775  rexanuz2nf  45803  evthiccabs  45809  ellimcabssub0  45930  climf  45935  clim2f  45947  clim2cf  45961  clim0cf  45965  limsupmnflem  46031  limsupre2lem  46035  limsupreuzmpt  46050  supcnvlimsup  46051  limsupge  46072  liminfreuzlem  46113  liminfltlem  46115  liminflimsupclim  46118  liminfpnfuz  46127  xlimpnfxnegmnf2  46169  fourierdlem70  46487  fourierdlem71  46488  fourierdlem73  46490  fourierdlem80  46497  fourierdlem83  46500  fourierdlem87  46504  voliunsge0lem  46783  meaiuninclem  46791  meaiuninc3v  46795  hoidmv1lelem3  46904  hoidmvlelem4  46909  hoidmvlelem5  46910  issmflem  47038  chnerlem1  47193  cfsetsnfsetf  47371  cfsetsnfsetfo  47373  requad2  47936  isubgrgrim  48242  grlicref  48325  islinindfis  48762  elbigolo1  48870  line2x  49067  itscnhlinecirc02p  49098  iscnrm3lem1  49246  ipolublem  49298  ipoglblem  49301  oppcup  49519  uptrlem3  49524  initopropd  49555  termopropd  49556  isinito2lem  49810  termc2  49830  lanup  49953  ranup  49954  aacllem  50113