Theorem ralbidva 3196

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143

This theorem is referenced by:  ralbidv  3197  2ralbidva  3198  raleqbidva  3425  poinxp  5632  soinxp  5633  frinxp  5634  ordunisssuc  6293  fnmptfvd  6811  funimass3  6824  fnnfpeq0  6940  cocan1  7047  cocan2  7048  isores2  7086  isoini2  7092  ofrfval  7417  ofrfval2  7427  tfindsg2  7576  f1oweALT  7673  fnsuppres  7857  dfsmo2  7984  smores  7989  smores2  7991  dfrecs3  8009  ac6sfi  8762  fimaxg  8765  ordunifi  8768  isfinite2  8776  fipreima  8830  supisolem  8937  fiming  8962  infempty  8971  ordiso2  8979  ordtypelem7  8988  cantnf  9156  wemapwe  9160  rankval3b  9255  rankonidlem  9257  iscard  9404  acndom  9477  dfac12lem3  9571  kmlem2  9577  cflim2  9685  cfsmolem  9692  ttukeylem6  9936  alephreg  10004  suplem2pr  10475  axsup  10716  sup3  11598  infm3  11600  suprleub  11607  dfinfre  11622  infregelb  11625  ofsubeq0  11635  ofsubge0  11637  zextlt  12057  prime  12064  suprfinzcl  12098  indstr  12317  supxr2  12708  supxrbnd1  12715  supxrbnd2  12716  supxrleub  12720  supxrbnd  12722  infxrgelb  12729  fzshftral  12996  mptnn0fsupp  13366  swrdspsleq  14027  pfxeq  14058  clim  14851  rlim  14852  clim2  14861  clim2c  14862  clim0c  14864  ello1mpt  14878  lo1o1  14889  o1lo1  14894  climabs0  14942  o1compt  14944  rlimdiv  15002  geomulcvg  15232  mertenslem2  15241  mertens  15242  rpnnen2lem12  15578  sqrt2irr  15602  fprodfvdvdsd  15683  fproddvdsd  15684  dfgcd2  15894  isprm7  16052  pc11  16216  pcz  16217  1arith  16263  vdwlem8  16324  vdwlem11  16327  vdw  16330  ramval  16344  pwsle  16765  mrieqvd  16909  mreacs  16929  cidpropd  16980  ismon2  17004  monpropd  17007  isepi  17010  isepi2  17011  subsubc  17123  funcres2b  17167  funcpropd  17170  isfull2  17181  isfth2  17185  fucsect  17242  fucinv  17243  pospropd  17744  ipodrsfi  17773  tsrss  17833  grpidpropd  17872  mndpropd  17936  smndex1mnd  18075  grppropd  18118  issubg4  18298  gass  18431  gsmsymgrfixlem1  18555  gsmsymgreqlem2  18559  gexdvds  18709  gexdvds2  18710  subgpgp  18722  sylow3lem6  18757  efgval2  18850  efgsp1  18863  dprdf11  19145  subgdmdprd  19156  ringpropd  19332  abvpropd  19613  lsspropd  19789  lbspropd  19871  assapropd  20101  psrbaglefi  20152  psrbagconf1o  20154  gsumbagdiaglem  20155  mplmonmul  20245  gsumply1eq  20473  phlpropd  20799  ishil2  20863  frlmplusgvalb  20913  frlmvscavalb  20914  frlmvplusgscavalb  20915  lindfmm  20971  islindf4  20982  islindf5  20983  scmatf1  21140  cpmatmcllem  21326  cpmatmcl  21327  decpmataa0  21376  decpmatmulsumfsupp  21381  pmatcollpw2lem  21385  pm2mpmhmlem1  21426  tgss2  21595  isclo  21695  neips  21721  opnnei  21728  isperf3  21761  ssidcn  21863  lmbrf  21868  cnnei  21890  cnrest2  21894  lmss  21906  lmres  21908  ist1-2  21955  ist1-3  21957  isreg2  21985  cmpfi  22016  bwth  22018  1stccn  22071  subislly  22089  kgencn  22164  ptclsg  22223  ptcnplem  22229  xkococnlem  22267  xkoinjcn  22295  tgqtop  22320  qtopcn  22322  fbflim  22584  flimrest  22591  flfnei  22599  isflf  22601  cnflf  22610  fclsopn  22622  fclsbas  22629  fclsrest  22632  isfcf  22642  cnfcf  22650  ptcmplem3  22662  tmdgsum2  22704  eltsms  22741  tsmsgsum  22747  tsmssubm  22751  tsmsf1o  22753  utopsnneiplem  22856  ismet2  22943  prdsxmetlem  22978  elmopn2  23055  prdsbl  23101  metss  23118  metrest  23134  metcnp  23151  metcnp2  23152  metcn  23153  metucn  23181  nrginvrcn  23301  metdsge  23457  divcn  23476  elcncf2  23498  mulc1cncf  23513  cncfmet  23516  evth2  23564  lmmbr2  23862  lmmbrf  23865  iscfil2  23869  cfil3i  23872  iscau2  23880  iscau4  23882  iscauf  23883  caucfil  23886  iscmet3lem3  23893  cfilres  23899  causs  23901  lmclim  23906  rrxmet  24011  evthicc2  24061  cniccbdd  24062  ovolfioo  24068  ovolficc  24069  ismbl2  24128  mbfsup  24265  mbfinf  24266  mbflimsup  24267  0plef  24273  mbfi1flim  24324  xrge0f  24332  itg2mulclem  24347  itgeqa  24414  ellimc2  24475  ellimc3  24477  limcflf  24479  cnlimc  24486  dvferm1  24582  dvferm2  24584  rolle  24587  dvivthlem1  24605  ftc1lem6  24638  itgsubst  24646  mdegle0  24671  deg1leb  24689  plydivex  24886  ulm2  24973  ulmcaulem  24982  ulmcau  24983  ulmdvlem3  24990  abelthlem9  25028  abelth  25029  rlimcnp  25543  ftalem3  25652  issqf  25713  sqf11  25716  dvdsmulf1o  25771  dchrelbas4  25819  dchrinv  25837  2sqlem6  25999  chpo1ubb  26057  dchrmusumlema  26069  dchrisum0lema  26090  ostth3  26214  tgcgr4  26317  eqeelen  26690  brbtwn2  26691  colinearalg  26696  axcgrid  26702  axsegconlem1  26703  ax5seglem4  26718  ax5seglem5  26719  axbtwnid  26725  axpasch  26727  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem12  26761  elntg2  26771  isuvtx  27177  uvtx2vtx1edg  27180  uvtx2vtx1edgb  27181  iscplgrnb  27198  iscplgredg  27199  vdiscusgrb  27312  uhgrvd00  27316  upgriswlk  27422  wwlksnext  27671  clwwlkinwwlk  27818  clwwlkel  27825  clwwlkf  27826  clwwlkwwlksb  27833  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  clwwlknonex2lem2  27887  nmounbi  28553  blocnilem  28581  isph  28599  phoeqi  28634  h2hcau  28756  h2hlm  28757  hial2eq2  28884  hoeq1  29607  hoeq2  29608  adjsym  29610  cnvadj  29669  hhcno  29681  hhcnf  29682  adjvalval  29714  leop2  29901  leoptri  29913  mdbr2  30073  dmdbr2  30080  mddmd2  30086  cdj3lem3b  30217  infxrge0gelb  30490  toslublem  30654  tosglblem  30656  submarchi  30815  isarchi3  30816  lindfpropd  30942  cmpcref  31114  lmdvg  31196  prodindf  31282  eulerpartlemd  31624  subfacp1lem3  32429  subfacp1lem5  32431  satfv1lem  32609  dfrdg2  33040  sltrec  33278  opnrebl  33668  poimirlem23  34930  broucube  34941  itg2gt0cn  34962  ftc1cnnc  34981  lmclim2  35048  caures  35050  sstotbnd2  35067  rrnmet  35122  rrncmslem  35125  isdrngo3  35252  isidlc  35308  cvrval2  36425  isat3  36458  iscvlat2N  36475  glbconN  36528  ltrneq  37300  cdlemefrs29clN  37550  cdlemefrs32fva  37551  cdleme32fva  37588  cdlemk33N  38060  cdlemk34  38061  cdlemkid3N  38084  cdlemkid4  38085  diaglbN  38206  dibglbN  38317  dihglbcpreN  38451  dihglblem6  38491  hdmap1eulem  38973  hdmap1eulemOLDN  38974  hdmapoc  39082  hlhilocv  39108  wepwsolem  39691  fnwe2lem2  39700  islnm2  39727  iscard5  39950  alephiso2  39966  clsk3nimkb  40439  ntrclsneine0  40464  ntrneineine0  40486  ntrneineine1  40487  ntrneicls00  40488  ntrneicls11  40489  ntrneiiso  40490  ntrneik2  40491  ntrneix2  40492  ntrneikb  40493  ntrneixb  40494  ntrneik3  40495  ntrneix3  40496  ntrneik13  40497  ntrneix13  40498  ntrneik4w  40499  ntrneik4  40500  caofcan  40704  infxrbnd2  41686  supminfxr  41789  evthiccabs  41820  ellimcabssub0  41947  climf  41952  clim2f  41966  clim2cf  41980  clim0cf  41984  limsupmnflem  42050  limsupre2lem  42054  limsupreuzmpt  42069  supcnvlimsup  42070  limsupge  42091  liminfreuzlem  42132  liminfltlem  42134  liminflimsupclim  42137  liminfpnfuz  42146  xlimpnfxnegmnf2  42188  fourierdlem70  42510  fourierdlem71  42511  fourierdlem73  42513  fourierdlem80  42520  fourierdlem83  42523  fourierdlem87  42527  voliunsge0lem  42803  meaiuninclem  42811  meaiuninc3v  42815  hoidmv1lelem3  42924  hoidmvlelem4  42929  hoidmvlelem5  42930  issmflem  43053  requad2  43837  islinindfis  44553  elbigolo1  44666  line2x  44790  itscnhlinecirc02p  44821  aacllem  44951