Theorem ralbidva 3117

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 3116	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2110  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3066

This theorem is referenced by:  ralbidv  3118  2ralbidva  3119  raleqbidva  3331  poinxp  5629  soinxp  5630  frinxp  5631  ordunisssuc  6315  fnmptfvd  6861  funimass3  6874  fnnfpeq0  6993  cocan1  7101  cocan2  7102  isores2  7142  isoini2  7148  ofrfvalg  7476  ofrfval2  7489  tfindsg2  7640  f1oweALT  7745  fnsuppres  7933  dfsmo2  8084  smores  8089  smores2  8091  dfrecs3  8109  ac6sfi  8915  fimaxg  8918  ordunifi  8921  isfinite2  8929  fipreima  8982  supisolem  9089  fiming  9114  infempty  9123  ordiso2  9131  ordtypelem7  9140  cantnf  9308  wemapwe  9312  rankval3b  9442  rankonidlem  9444  iscard  9591  acndom  9665  dfac12lem3  9759  kmlem2  9765  cflim2  9877  cfsmolem  9884  ttukeylem6  10128  alephreg  10196  suplem2pr  10667  axsup  10908  sup3  11789  infm3  11791  suprleub  11798  dfinfre  11813  infregelb  11816  ofsubeq0  11827  ofsubge0  11829  zextlt  12251  prime  12258  suprfinzcl  12292  indstr  12512  supxr2  12904  supxrbnd1  12911  supxrbnd2  12912  supxrleub  12916  supxrbnd  12918  infxrgelb  12925  fzshftral  13200  mptnn0fsupp  13570  swrdspsleq  14230  pfxeq  14261  clim  15055  rlim  15056  clim2  15065  clim2c  15066  clim0c  15068  ello1mpt  15082  lo1o1  15093  o1lo1  15098  climabs0  15146  o1compt  15148  rlimdiv  15209  geomulcvg  15440  mertenslem2  15449  mertens  15450  rpnnen2lem12  15786  sqrt2irr  15810  fprodfvdvdsd  15895  fproddvdsd  15896  dfgcd2  16106  isprm7  16265  pc11  16433  pcz  16434  1arith  16480  vdwlem8  16541  vdwlem11  16544  vdw  16547  ramval  16561  pwsle  16997  mrieqvd  17141  mreacs  17161  cidpropd  17213  ismon2  17239  monpropd  17242  isepi  17245  isepi2  17246  subsubc  17359  funcres2b  17403  funcpropd  17407  isfull2  17418  isfth2  17422  fucsect  17481  fucinv  17482  pospropd  17833  ipodrsfi  18045  tsrss  18095  grpidpropd  18134  mndpropd  18198  smndex1mnd  18337  grppropd  18382  issubg4  18562  gass  18695  gsmsymgrfixlem1  18819  gsmsymgreqlem2  18823  gexdvds  18973  gexdvds2  18974  subgpgp  18986  sylow3lem6  19021  efgval2  19114  efgsp1  19127  dprdf11  19410  subgdmdprd  19421  ringpropd  19600  abvpropd  19878  lsspropd  20054  lbspropd  20136  phlpropd  20617  ishil2  20681  frlmplusgvalb  20731  frlmvscavalb  20732  frlmvplusgscavalb  20733  lindfmm  20789  islindf4  20800  islindf5  20801  assapropd  20831  psrbaglefi  20891  psrbaglefiOLD  20892  psrbagconf1o  20895  psrbagconf1oOLD  20896  gsumbagdiaglemOLD  20897  gsumbagdiaglem  20900  mplmonmul  20993  gsumply1eq  21226  scmatf1  21428  cpmatmcllem  21615  cpmatmcl  21616  decpmataa0  21665  decpmatmulsumfsupp  21670  pmatcollpw2lem  21674  pm2mpmhmlem1  21715  tgss2  21884  isclo  21984  neips  22010  opnnei  22017  isperf3  22050  ssidcn  22152  lmbrf  22157  cnnei  22179  cnrest2  22183  lmss  22195  lmres  22197  ist1-2  22244  ist1-3  22246  isreg2  22274  cmpfi  22305  bwth  22307  1stccn  22360  subislly  22378  kgencn  22453  ptclsg  22512  ptcnplem  22518  xkococnlem  22556  xkoinjcn  22584  tgqtop  22609  qtopcn  22611  fbflim  22873  flimrest  22880  flfnei  22888  isflf  22890  cnflf  22899  fclsopn  22911  fclsbas  22918  fclsrest  22921  isfcf  22931  cnfcf  22939  ptcmplem3  22951  tmdgsum2  22993  eltsms  23030  tsmsgsum  23036  tsmssubm  23040  tsmsf1o  23042  utopsnneiplem  23145  ismet2  23231  prdsxmetlem  23266  elmopn2  23343  prdsbl  23389  metss  23406  metrest  23422  metcnp  23439  metcnp2  23440  metcn  23441  metucn  23469  nrginvrcn  23590  metdsge  23746  divcn  23765  elcncf2  23787  mulc1cncf  23802  cncfmet  23806  evth2  23857  lmmbr2  24156  lmmbrf  24159  iscfil2  24163  cfil3i  24166  iscau2  24174  iscau4  24176  iscauf  24177  caucfil  24180  iscmet3lem3  24187  cfilres  24193  causs  24195  lmclim  24200  rrxmet  24305  evthicc2  24357  cniccbdd  24358  ovolfioo  24364  ovolficc  24365  ismbl2  24424  mbfsup  24561  mbfinf  24562  mbflimsup  24563  0plef  24569  mbfi1flim  24621  xrge0f  24629  itg2mulclem  24644  itgeqa  24711  ellimc2  24774  ellimc3  24776  limcflf  24778  cnlimc  24785  dvferm1  24882  dvferm2  24884  rolle  24887  dvivthlem1  24905  ftc1lem6  24938  itgsubst  24946  mdegle0  24975  deg1leb  24993  plydivex  25190  ulm2  25277  ulmcaulem  25286  ulmcau  25287  ulmdvlem3  25294  abelthlem9  25332  abelth  25333  rlimcnp  25848  ftalem3  25957  issqf  26018  sqf11  26021  dvdsmulf1o  26076  dchrelbas4  26124  dchrinv  26142  2sqlem6  26304  chpo1ubb  26362  dchrmusumlema  26374  dchrisum0lema  26395  ostth3  26519  tgcgr4  26622  eqeelen  26995  brbtwn2  26996  colinearalg  27001  axcgrid  27007  axsegconlem1  27008  ax5seglem4  27023  ax5seglem5  27024  axbtwnid  27030  axpasch  27032  axeuclidlem  27053  axcontlem2  27056  axcontlem4  27058  axcontlem7  27061  axcontlem12  27066  elntg2  27076  isuvtx  27483  uvtx2vtx1edg  27486  uvtx2vtx1edgb  27487  iscplgrnb  27504  iscplgredg  27505  vdiscusgrb  27618  uhgrvd00  27622  upgriswlk  27728  wwlksnext  27977  clwwlkinwwlk  28123  clwwlkel  28129  clwwlkf  28130  clwwlkwwlksb  28137  wwlksext2clwwlk  28140  wwlksubclwwlk  28141  clwwlknonex2lem2  28191  nmounbi  28857  blocnilem  28885  isph  28903  phoeqi  28938  h2hcau  29060  h2hlm  29061  hial2eq2  29188  hoeq1  29911  hoeq2  29912  adjsym  29914  cnvadj  29973  hhcno  29985  hhcnf  29986  adjvalval  30018  leop2  30205  leoptri  30217  mdbr2  30377  dmdbr2  30384  mddmd2  30390  cdj3lem3b  30521  infxrge0gelb  30809  toslublem  30969  tosglblem  30971  mgccnv  30996  submarchi  31159  isarchi3  31160  lindfpropd  31290  cmpcref  31514  lmdvg  31617  prodindf  31703  eulerpartlemd  32045  subfacp1lem3  32857  subfacp1lem5  32859  satfv1lem  33037  dfrdg2  33490  sltrec  33751  lrrecfr  33837  opnrebl  34246  poimirlem23  35537  broucube  35548  itg2gt0cn  35569  ftc1cnnc  35586  lmclim2  35653  caures  35655  sstotbnd2  35669  rrnmet  35724  rrncmslem  35727  isdrngo3  35854  isidlc  35910  cvrval2  37025  isat3  37058  iscvlat2N  37075  glbconN  37128  ltrneq  37900  cdlemefrs29clN  38150  cdlemefrs32fva  38151  cdleme32fva  38188  cdlemk33N  38660  cdlemk34  38661  cdlemkid3N  38684  cdlemkid4  38685  diaglbN  38806  dibglbN  38917  dihglbcpreN  39051  dihglblem6  39091  hdmap1eulem  39573  hdmap1eulemOLDN  39574  hdmapoc  39682  hlhilocv  39708  wepwsolem  40570  fnwe2lem2  40579  islnm2  40606  iscard5  40826  alephiso2  40841  clsk3nimkb  41327  ntrclsneine0  41352  ntrneineine0  41374  ntrneineine1  41375  ntrneicls00  41376  ntrneicls11  41377  ntrneiiso  41378  ntrneik2  41379  ntrneix2  41380  ntrneikb  41381  ntrneixb  41382  ntrneik3  41383  ntrneix3  41384  ntrneik13  41385  ntrneix13  41386  ntrneik4w  41387  ntrneik4  41388  caofcan  41614  infxrbnd2  42581  supminfxr  42679  evthiccabs  42709  ellimcabssub0  42833  climf  42838  clim2f  42852  clim2cf  42866  clim0cf  42870  limsupmnflem  42936  limsupre2lem  42940  limsupreuzmpt  42955  supcnvlimsup  42956  limsupge  42977  liminfreuzlem  43018  liminfltlem  43020  liminflimsupclim  43023  liminfpnfuz  43032  xlimpnfxnegmnf2  43074  fourierdlem70  43392  fourierdlem71  43393  fourierdlem73  43395  fourierdlem80  43402  fourierdlem83  43405  fourierdlem87  43409  voliunsge0lem  43685  meaiuninclem  43693  meaiuninc3v  43697  hoidmv1lelem3  43806  hoidmvlelem4  43811  hoidmvlelem5  43812  issmflem  43935  cfsetsnfsetf  44224  cfsetsnfsetfo  44226  requad2  44748  islinindfis  45463  elbigolo1  45576  line2x  45773  itscnhlinecirc02p  45804  iscnrm3lem1  45900  ipolublem  45945  ipoglblem  45948  aacllem  46176