Theorem ralbidva 3176

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  ralbidv  3178  2ralbidva  3217  raleqbidva  3328  poinxp  5757  soinxp  5758  frinxp  5759  ordunisssuc  6471  fnmptfvd  7043  funimass3  7056  fnnfpeq0  7176  cocan1  7289  cocan2  7290  isores2  7330  isoini2  7336  ofrfvalg  7678  ofrfval2  7691  tfindsg2  7851  f1oweALT  7959  fnsuppres  8176  dfsmo2  8347  smores  8352  smores2  8354  dfrecs3  8372  dfrecs3OLD  8373  naddunif  8692  ac6sfi  9287  fimaxg  9290  ordunifi  9293  isfinite2  9301  fipreima  9358  supisolem  9468  fiming  9493  infempty  9502  ordiso2  9510  ordtypelem7  9519  cantnf  9688  wemapwe  9692  rankval3b  9821  rankonidlem  9823  iscard  9970  acndom  10046  dfac12lem3  10140  kmlem2  10146  cflim2  10258  cfsmolem  10265  ttukeylem6  10509  alephreg  10577  suplem2pr  11048  axsup  11289  sup3  12171  infm3  12173  suprleub  12180  dfinfre  12195  infregelb  12198  ofsubeq0  12209  ofsubge0  12211  zextlt  12636  prime  12643  suprfinzcl  12676  indstr  12900  supxr2  13293  supxrbnd1  13300  supxrbnd2  13301  supxrleub  13305  supxrbnd  13307  infxrgelb  13314  fzshftral  13589  mptnn0fsupp  13962  swrdspsleq  14615  pfxeq  14646  clim  15438  rlim  15439  clim2  15448  clim2c  15449  clim0c  15451  ello1mpt  15465  lo1o1  15476  o1lo1  15481  climabs0  15529  o1compt  15531  rlimdiv  15592  geomulcvg  15822  mertenslem2  15831  mertens  15832  rpnnen2lem12  16168  sqrt2irr  16192  fprodfvdvdsd  16277  fproddvdsd  16278  dfgcd2  16488  isprm7  16645  pc11  16813  pcz  16814  1arith  16860  vdwlem8  16921  vdwlem11  16924  vdw  16927  ramval  16941  pwsle  17438  mrieqvd  17582  mreacs  17602  cidpropd  17654  ismon2  17681  monpropd  17684  isepi  17687  isepi2  17688  subsubc  17803  funcres2b  17847  funcpropd  17851  isfull2  17862  isfth2  17866  fucsect  17925  fucinv  17926  pospropd  18280  ipodrsfi  18492  tsrss  18542  grpidpropd  18581  sgrppropd  18622  mndpropd  18650  smndex1mnd  18791  grppropd  18837  issubg4  19025  gass  19165  gsmsymgrfixlem1  19295  gsmsymgreqlem2  19299  gexdvds  19452  gexdvds2  19453  subgpgp  19465  sylow3lem6  19500  efgval2  19592  efgsp1  19605  dprdf11  19893  subgdmdprd  19904  ringpropd  20102  abvpropd  20450  lsspropd  20628  lbspropd  20710  isridl  20859  phlpropd  21208  ishil2  21274  frlmplusgvalb  21324  frlmvscavalb  21325  frlmvplusgscavalb  21326  lindfmm  21382  islindf4  21393  islindf5  21394  assapropd  21426  psrbaglefi  21485  psrbaglefiOLD  21486  psrbagconf1o  21489  psrbagconf1oOLD  21490  gsumbagdiaglemOLD  21491  gsumbagdiaglem  21494  mplmonmul  21591  gsumply1eq  21829  scmatf1  22033  cpmatmcllem  22220  cpmatmcl  22221  decpmataa0  22270  decpmatmulsumfsupp  22275  pmatcollpw2lem  22279  pm2mpmhmlem1  22320  tgss2  22490  isclo  22591  neips  22617  opnnei  22624  isperf3  22657  ssidcn  22759  lmbrf  22764  cnnei  22786  cnrest2  22790  lmss  22802  lmres  22804  ist1-2  22851  ist1-3  22853  isreg2  22881  cmpfi  22912  bwth  22914  1stccn  22967  subislly  22985  kgencn  23060  ptclsg  23119  ptcnplem  23125  xkococnlem  23163  xkoinjcn  23191  tgqtop  23216  qtopcn  23218  fbflim  23480  flimrest  23487  flfnei  23495  isflf  23497  cnflf  23506  fclsopn  23518  fclsbas  23525  fclsrest  23528  isfcf  23538  cnfcf  23546  ptcmplem3  23558  tmdgsum2  23600  eltsms  23637  tsmsgsum  23643  tsmssubm  23647  tsmsf1o  23649  utopsnneiplem  23752  ismet2  23839  prdsxmetlem  23874  elmopn2  23951  prdsbl  24000  metss  24017  metrest  24033  metcnp  24050  metcnp2  24051  metcn  24052  metucn  24080  nrginvrcn  24209  metdsge  24365  divcn  24384  elcncf2  24406  mulc1cncf  24421  cncfmet  24425  evth2  24476  lmmbr2  24776  lmmbrf  24779  iscfil2  24783  cfil3i  24786  iscau2  24794  iscau4  24796  iscauf  24797  caucfil  24800  iscmet3lem3  24807  cfilres  24813  causs  24815  lmclim  24820  rrxmet  24925  evthicc2  24977  cniccbdd  24978  ovolfioo  24984  ovolficc  24985  ismbl2  25044  mbfsup  25181  mbfinf  25182  mbflimsup  25183  0plef  25189  mbfi1flim  25241  xrge0f  25249  itg2mulclem  25264  itgeqa  25331  ellimc2  25394  ellimc3  25396  limcflf  25398  cnlimc  25405  dvferm1  25502  dvferm2  25504  rolle  25507  dvivthlem1  25525  ftc1lem6  25558  itgsubst  25566  mdegle0  25595  deg1leb  25613  plydivex  25810  ulm2  25897  ulmcaulem  25906  ulmcau  25907  ulmdvlem3  25914  abelthlem9  25952  abelth  25953  rlimcnp  26470  ftalem3  26579  issqf  26640  sqf11  26643  dvdsmulf1o  26698  dchrelbas4  26746  dchrinv  26764  2sqlem6  26926  chpo1ubb  26984  dchrmusumlema  26996  dchrisum0lema  27017  ostth3  27141  sltrec  27321  lrrecfr  27427  addsuniflem  27484  negsunif  27529  tgcgr4  27782  eqeelen  28162  brbtwn2  28163  colinearalg  28168  axcgrid  28174  axsegconlem1  28175  ax5seglem4  28190  ax5seglem5  28191  axbtwnid  28197  axpasch  28199  axeuclidlem  28220  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  axcontlem12  28233  elntg2  28243  isuvtx  28652  uvtx2vtx1edg  28655  uvtx2vtx1edgb  28656  iscplgrnb  28673  iscplgredg  28674  vdiscusgrb  28787  uhgrvd00  28791  upgriswlk  28898  wwlksnext  29147  clwwlkinwwlk  29293  clwwlkel  29299  clwwlkf  29300  clwwlkwwlksb  29307  wwlksext2clwwlk  29310  wwlksubclwwlk  29311  clwwlknonex2lem2  29361  nmounbi  30029  blocnilem  30057  isph  30075  phoeqi  30110  h2hcau  30232  h2hlm  30233  hial2eq2  30360  hoeq1  31083  hoeq2  31084  adjsym  31086  cnvadj  31145  hhcno  31157  hhcnf  31158  adjvalval  31190  leop2  31377  leoptri  31389  mdbr2  31549  dmdbr2  31556  mddmd2  31562  cdj3lem3b  31693  infxrge0gelb  31979  toslublem  32142  tosglblem  32144  mgccnv  32169  submarchi  32332  isarchi3  32333  lindfpropd  32498  opprlidlabs  32599  ply1moneq  32665  cmpcref  32830  lmdvg  32933  prodindf  33021  eulerpartlemd  33365  subfacp1lem3  34173  subfacp1lem5  34175  satfv1lem  34353  dfrdg2  34767  gg-divcn  35163  opnrebl  35205  poimirlem23  36511  broucube  36522  itg2gt0cn  36543  ftc1cnnc  36560  lmclim2  36626  caures  36628  sstotbnd2  36642  rrnmet  36697  rrncmslem  36700  isdrngo3  36827  isidlc  36883  cvrval2  38144  isat3  38177  iscvlat2N  38194  glbconN  38247  glbconNOLD  38248  ltrneq  39020  cdlemefrs29clN  39270  cdlemefrs32fva  39271  cdleme32fva  39308  cdlemk33N  39780  cdlemk34  39781  cdlemkid3N  39804  cdlemkid4  39805  diaglbN  39926  dibglbN  40037  dihglbcpreN  40171  dihglblem6  40211  hdmap1eulem  40693  hdmap1eulemOLDN  40694  hdmapoc  40802  hlhilocv  40832  wepwsolem  41784  fnwe2lem2  41793  islnm2  41820  onmaxnelsup  41972  onsupnmax  41977  onsupuni  41978  onsupmaxb  41988  onsupeqnmax  41996  iscard5  42287  alephiso2  42309  clsk3nimkb  42791  ntrclsneine0  42816  ntrneineine0  42838  ntrneineine1  42839  ntrneicls00  42840  ntrneicls11  42841  ntrneiiso  42842  ntrneik2  42843  ntrneix2  42844  ntrneikb  42845  ntrneixb  42846  ntrneik3  42847  ntrneix3  42848  ntrneik13  42849  ntrneix13  42850  ntrneik4w  42851  ntrneik4  42852  caofcan  43082  infxrbnd2  44079  supminfxr  44174  rexanuz2nf  44203  evthiccabs  44209  ellimcabssub0  44333  climf  44338  clim2f  44352  clim2cf  44366  clim0cf  44370  limsupmnflem  44436  limsupre2lem  44440  limsupreuzmpt  44455  supcnvlimsup  44456  limsupge  44477  liminfreuzlem  44518  liminfltlem  44520  liminflimsupclim  44523  liminfpnfuz  44532  xlimpnfxnegmnf2  44574  fourierdlem70  44892  fourierdlem71  44893  fourierdlem73  44895  fourierdlem80  44902  fourierdlem83  44905  fourierdlem87  44909  voliunsge0lem  45188  meaiuninclem  45196  meaiuninc3v  45200  hoidmv1lelem3  45309  hoidmvlelem4  45314  hoidmvlelem5  45315  issmflem  45443  cfsetsnfsetf  45768  cfsetsnfsetfo  45770  requad2  46291  rngpropd  46673  isridlrng  46751  islinindfis  47130  elbigolo1  47243  line2x  47440  itscnhlinecirc02p  47471  iscnrm3lem1  47566  ipolublem  47611  ipoglblem  47614  aacllem  47848