Theorem ralbidva 3159

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 3157	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  3161  2ralbidva  3200  raleqbidva  3302  poinxp  5703  soinxp  5704  frinxp  5705  ordunisssuc  6423  fnmptfvd  6985  funimass3  6998  fnnfpeq0  7124  cocan1  7237  cocan2  7238  isores2  7279  isoini2  7285  ofrfvalg  7630  ofrfval2  7643  caofidlcan  7660  tfindsg2  7804  f1oweALT  7916  fnsuppres  8132  dfsmo2  8278  smores  8283  smores2  8285  dfrecs3  8303  naddunif  8620  ac6sfi  9185  fimaxg  9188  ordunifi  9191  isfinite2  9199  fipreima  9259  supisolem  9378  fiming  9404  infempty  9413  ordiso2  9421  ordtypelem7  9430  cantnf  9603  wemapwe  9607  rankval3b  9739  rankonidlem  9741  iscard  9888  acndom  9962  dfac12lem3  10057  kmlem2  10063  cflim2  10174  cfsmolem  10181  ttukeylem6  10425  alephreg  10494  suplem2pr  10965  axsup  11209  sup3  12100  infm3  12102  suprleub  12109  dfinfre  12124  infregelb  12127  ofsubeq0  12143  ofsubge0  12145  zextlt  12567  prime  12574  suprfinzcl  12607  indstr  12830  supxr2  13230  supxrbnd1  13237  supxrbnd2  13238  supxrleub  13242  supxrbnd  13244  infxrgelb  13252  fzshftral  13532  mptnn0fsupp  13921  swrdspsleq  14590  pfxeq  14620  clim  15418  rlim  15419  clim2  15428  clim2c  15429  clim0c  15431  ello1mpt  15445  lo1o1  15456  o1lo1  15461  climabs0  15509  o1compt  15511  rlimdiv  15570  geomulcvg  15800  mertenslem2  15809  mertens  15810  rpnnen2lem12  16151  sqrt2irr  16175  fprodfvdvdsd  16262  fproddvdsd  16263  dfgcd2  16474  isprm7  16636  pc11  16809  pcz  16810  1arith  16856  vdwlem8  16917  vdwlem11  16920  vdw  16923  ramval  16937  pwsle  17414  mrieqvd  17562  mreacs  17582  cidpropd  17634  ismon2  17659  monpropd  17662  isepi  17665  isepi2  17666  subsubc  17778  funcres2b  17822  funcpropd  17827  isfull2  17838  isfth2  17842  fucsect  17900  fucinv  17901  pospropd  18249  ipodrsfi  18463  tsrss  18513  grpidpropd  18588  sgrppropd  18657  mndpropd  18685  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  20770  lsspropd  20971  lbspropd  21053  isridlrng  21176  isridl  21209  phlpropd  21612  ishil2  21676  frlmplusgvalb  21726  frlmvscavalb  21727  frlmvplusgscavalb  21728  lindfmm  21784  islindf4  21795  islindf5  21796  assapropd  21828  psrbaglefi  21883  psrbagconf1o  21886  gsumbagdiaglem  21887  mplmonmul  21992  gsumply1eq  22252  scmatf1  22474  cpmatmcllem  22661  cpmatmcl  22662  decpmataa0  22711  decpmatmulsumfsupp  22716  pmatcollpw2lem  22720  pm2mpmhmlem1  22761  tgss2  22930  isclo  23030  neips  23056  opnnei  23063  isperf3  23096  ssidcn  23198  lmbrf  23203  cnnei  23225  cnrest2  23229  lmss  23241  lmres  23243  ist1-2  23290  ist1-3  23292  isreg2  23320  cmpfi  23351  bwth  23353  1stccn  23406  subislly  23424  kgencn  23499  ptclsg  23558  ptcnplem  23564  xkococnlem  23602  xkoinjcn  23630  tgqtop  23655  qtopcn  23657  fbflim  23919  flimrest  23926  flfnei  23934  isflf  23936  cnflf  23945  fclsopn  23957  fclsbas  23964  fclsrest  23967  isfcf  23977  cnfcf  23985  ptcmplem3  23997  tmdgsum2  24039  eltsms  24076  tsmsgsum  24082  tsmssubm  24086  tsmsf1o  24088  utopsnneiplem  24190  ismet2  24276  prdsxmetlem  24311  elmopn2  24388  prdsbl  24434  metss  24451  metrest  24467  metcnp  24484  metcnp2  24485  metcn  24486  metucn  24514  nrginvrcn  24635  metdsge  24793  divcn  24813  elcncf2  24835  mulc1cncf  24850  cncfmet  24854  evth2  24905  lmmbr2  25204  lmmbrf  25207  iscfil2  25211  cfil3i  25214  iscau2  25222  iscau4  25224  iscauf  25225  caucfil  25228  iscmet3lem3  25235  cfilres  25241  causs  25243  lmclim  25248  rrxmet  25353  evthicc2  25405  cniccbdd  25406  ovolfioo  25412  ovolficc  25413  ismbl2  25472  mbfsup  25609  mbfinf  25610  mbflimsup  25611  0plef  25617  mbfi1flim  25668  xrge0f  25676  itg2mulclem  25691  itgeqa  25759  ellimc2  25822  ellimc3  25824  limcflf  25826  cnlimc  25833  dvferm1  25930  dvferm2  25932  rolle  25935  dvivthlem1  25954  ftc1lem6  25989  itgsubst  25997  mdegle0  26023  deg1leb  26041  plydivex  26245  ulm2  26334  ulmcaulem  26343  ulmcau  26344  ulmdvlem3  26351  abelthlem9  26390  abelth  26391  rlimcnp  26915  ftalem3  27025  issqf  27086  sqf11  27089  mpodvdsmulf1o  27144  dvdsmulf1o  27146  dchrelbas4  27194  dchrinv  27212  2sqlem6  27374  chpo1ubb  27432  dchrmusumlema  27444  dchrisum0lema  27465  ostth3  27589  ltsrec  27781  lrrecfr  27923  addsuniflem  27981  addbday  27998  negsunif  28035  n0fincut  28335  bdayfinbndlem1  28447  elreno2  28475  tgcgr4  28587  eqeelen  28961  brbtwn2  28962  colinearalg  28967  axcgrid  28973  axsegconlem1  28974  ax5seglem4  28989  ax5seglem5  28990  axbtwnid  28996  axpasch  28998  axeuclidlem  29019  axcontlem2  29022  axcontlem4  29024  axcontlem7  29027  axcontlem12  29032  elntg2  29042  isuvtx  29452  uvtx2vtx1edg  29455  uvtx2vtx1edgb  29456  iscplgrnb  29473  iscplgredg  29474  vdiscusgrb  29588  uhgrvd00  29592  upgriswlk  29698  wwlksnext  29950  clwwlkinwwlk  30099  clwwlkel  30105  clwwlkf  30106  clwwlkwwlksb  30113  wwlksext2clwwlk  30116  wwlksubclwwlk  30117  clwwlknonex2lem2  30167  nmounbi  30836  blocnilem  30864  isph  30882  phoeqi  30917  h2hcau  31039  h2hlm  31040  hial2eq2  31167  hoeq1  31890  hoeq2  31891  adjsym  31893  cnvadj  31952  hhcno  31964  hhcnf  31965  adjvalval  31997  leop2  32184  leoptri  32196  mdbr2  32356  dmdbr2  32363  mddmd2  32369  cdj3lem3b  32500  infxrge0gelb  32829  prodindf  32927  toslublem  33037  tosglblem  33039  mgccnv  33064  cntrval2  33237  submarchi  33252  isarchi3  33253  lindfpropd  33447  opprlidlabs  33550  ply1moneq  33653  psrmonmul  33699  cmpcref  34000  lmdvg  34103  eulerpartlemd  34516  subfacp1lem3  35370  subfacp1lem5  35372  satfv1lem  35550  dfrdg2  35981  opnrebl  36508  poimirlem23  37955  broucube  37966  itg2gt0cn  37987  ftc1cnnc  38004  lmclim2  38070  caures  38072  sstotbnd2  38086  rrnmet  38141  rrncmslem  38144  isdrngo3  38271  isidlc  38327  cvrval2  39711  isat3  39744  iscvlat2N  39761  glbconN  39814  ltrneq  40586  cdlemefrs29clN  40836  cdlemefrs32fva  40837  cdleme32fva  40874  cdlemk33N  41346  cdlemk34  41347  cdlemkid3N  41370  cdlemkid4  41371  diaglbN  41492  dibglbN  41603  dihglbcpreN  41737  dihglblem6  41777  hdmap1eulem  42259  hdmap1eulemOLDN  42260  hdmapoc  42368  hlhilocv  42394  primrootsunit1  42528  sn-sup3d  42936  fimgmcyc  42978  wepwsolem  43473  fnwe2lem2  43482  islnm2  43509  onmaxnelsup  43654  onsupnmax  43659  onsupuni  43660  onsupmaxb  43670  onsupeqnmax  43678  iscard5  43966  alephiso2  43988  clsk3nimkb  44470  ntrclsneine0  44495  ntrneineine0  44517  ntrneineine1  44518  ntrneicls00  44519  ntrneicls11  44520  ntrneiiso  44521  ntrneik2  44522  ntrneix2  44523  ntrneikb  44524  ntrneixb  44525  ntrneik3  44526  ntrneix3  44527  ntrneik13  44528  ntrneix13  44529  ntrneik4w  44530  ntrneik4  44531  caofcan  44753  modelac8prim  45422  infxrbnd2  45801  supminfxr  45896  rexanuz2nf  45924  evthiccabs  45930  ellimcabssub0  46051  climf  46056  clim2f  46068  clim2cf  46082  clim0cf  46086  limsupmnflem  46152  limsupre2lem  46156  limsupreuzmpt  46171  supcnvlimsup  46172  limsupge  46193  liminfreuzlem  46234  liminfltlem  46236  liminflimsupclim  46239  liminfpnfuz  46248  xlimpnfxnegmnf2  46290  fourierdlem70  46608  fourierdlem71  46609  fourierdlem73  46611  fourierdlem80  46618  fourierdlem83  46621  fourierdlem87  46625  voliunsge0lem  46904  meaiuninclem  46912  meaiuninc3v  46916  hoidmv1lelem3  47025  hoidmvlelem4  47030  hoidmvlelem5  47031  issmflem  47159  chnerlem1  47314  cfsetsnfsetf  47492  cfsetsnfsetfo  47494  requad2  48057  isubgrgrim  48363  grlicref  48446  islinindfis  48883  elbigolo1  48991  line2x  49188  itscnhlinecirc02p  49219  iscnrm3lem1  49367  ipolublem  49419  ipoglblem  49422  oppcup  49640  uptrlem3  49645  initopropd  49676  termopropd  49677  isinito2lem  49931  termc2  49951  lanup  50074  ranup  50075  aacllem  50234