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  3304  poinxp  5715  soinxp  5716  frinxp  5717  ordunisssuc  6435  fnmptfvd  6997  funimass3  7010  fnnfpeq0  7136  cocan1  7249  cocan2  7250  isores2  7291  isoini2  7297  ofrfvalg  7642  ofrfval2  7655  caofidlcan  7672  tfindsg2  7816  f1oweALT  7928  fnsuppres  8145  dfsmo2  8291  smores  8296  smores2  8298  dfrecs3  8316  naddunif  8633  ac6sfi  9198  fimaxg  9201  ordunifi  9204  isfinite2  9212  fipreima  9272  supisolem  9391  fiming  9417  infempty  9426  ordiso2  9434  ordtypelem7  9443  cantnf  9616  wemapwe  9620  rankval3b  9752  rankonidlem  9754  iscard  9901  acndom  9975  dfac12lem3  10070  kmlem2  10076  cflim2  10187  cfsmolem  10194  ttukeylem6  10438  alephreg  10507  suplem2pr  10978  axsup  11222  sup3  12113  infm3  12115  suprleub  12122  dfinfre  12137  infregelb  12140  ofsubeq0  12156  ofsubge0  12158  zextlt  12580  prime  12587  suprfinzcl  12620  indstr  12843  supxr2  13243  supxrbnd1  13250  supxrbnd2  13251  supxrleub  13255  supxrbnd  13257  infxrgelb  13265  fzshftral  13545  mptnn0fsupp  13934  swrdspsleq  14603  pfxeq  14633  clim  15431  rlim  15432  clim2  15441  clim2c  15442  clim0c  15444  ello1mpt  15458  lo1o1  15469  o1lo1  15474  climabs0  15522  o1compt  15524  rlimdiv  15583  geomulcvg  15813  mertenslem2  15822  mertens  15823  rpnnen2lem12  16164  sqrt2irr  16188  fprodfvdvdsd  16275  fproddvdsd  16276  dfgcd2  16487  isprm7  16649  pc11  16822  pcz  16823  1arith  16869  vdwlem8  16930  vdwlem11  16933  vdw  16936  ramval  16950  pwsle  17427  mrieqvd  17575  mreacs  17595  cidpropd  17647  ismon2  17672  monpropd  17675  isepi  17678  isepi2  17679  subsubc  17791  funcres2b  17835  funcpropd  17840  isfull2  17851  isfth2  17855  fucsect  17913  fucinv  17914  pospropd  18262  ipodrsfi  18476  tsrss  18526  grpidpropd  18601  sgrppropd  18670  mndpropd  18698  smndex1mnd  18852  grppropd  18898  issubg4  19092  gass  19247  gsmsymgrfixlem1  19373  gsmsymgreqlem2  19377  gexdvds  19530  gexdvds2  19531  subgpgp  19543  sylow3lem6  19578  efgval2  19670  efgsp1  19683  dprdf11  19971  subgdmdprd  19982  rngpropd  20126  ringpropd  20240  abvpropd  20785  lsspropd  20986  lbspropd  21068  isridlrng  21191  isridl  21224  phlpropd  21627  ishil2  21691  frlmplusgvalb  21741  frlmvscavalb  21742  frlmvplusgscavalb  21743  lindfmm  21799  islindf4  21810  islindf5  21811  assapropd  21844  psrbaglefi  21899  psrbagconf1o  21902  gsumbagdiaglem  21903  mplmonmul  22008  gsumply1eq  22270  scmatf1  22492  cpmatmcllem  22679  cpmatmcl  22680  decpmataa0  22729  decpmatmulsumfsupp  22734  pmatcollpw2lem  22738  pm2mpmhmlem1  22779  tgss2  22948  isclo  23048  neips  23074  opnnei  23081  isperf3  23114  ssidcn  23216  lmbrf  23221  cnnei  23243  cnrest2  23247  lmss  23259  lmres  23261  ist1-2  23308  ist1-3  23310  isreg2  23338  cmpfi  23369  bwth  23371  1stccn  23424  subislly  23442  kgencn  23517  ptclsg  23576  ptcnplem  23582  xkococnlem  23620  xkoinjcn  23648  tgqtop  23673  qtopcn  23675  fbflim  23937  flimrest  23944  flfnei  23952  isflf  23954  cnflf  23963  fclsopn  23975  fclsbas  23982  fclsrest  23985  isfcf  23995  cnfcf  24003  ptcmplem3  24015  tmdgsum2  24057  eltsms  24094  tsmsgsum  24100  tsmssubm  24104  tsmsf1o  24106  utopsnneiplem  24208  ismet2  24294  prdsxmetlem  24329  elmopn2  24406  prdsbl  24452  metss  24469  metrest  24485  metcnp  24502  metcnp2  24503  metcn  24504  metucn  24532  nrginvrcn  24653  metdsge  24811  divcnOLD  24830  divcn  24832  elcncf2  24856  mulc1cncf  24871  cncfmet  24875  evth2  24932  lmmbr2  25232  lmmbrf  25235  iscfil2  25239  cfil3i  25242  iscau2  25250  iscau4  25252  iscauf  25253  caucfil  25256  iscmet3lem3  25263  cfilres  25269  causs  25271  lmclim  25276  rrxmet  25381  evthicc2  25434  cniccbdd  25435  ovolfioo  25441  ovolficc  25442  ismbl2  25501  mbfsup  25638  mbfinf  25639  mbflimsup  25640  0plef  25646  mbfi1flim  25697  xrge0f  25705  itg2mulclem  25720  itgeqa  25788  ellimc2  25851  ellimc3  25853  limcflf  25855  cnlimc  25862  dvferm1  25962  dvferm2  25964  rolle  25967  dvivthlem1  25986  ftc1lem6  26021  itgsubst  26029  mdegle0  26055  deg1leb  26073  plydivex  26278  ulm2  26367  ulmcaulem  26376  ulmcau  26377  ulmdvlem3  26384  abelthlem9  26423  abelth  26424  rlimcnp  26948  ftalem3  27058  issqf  27119  sqf11  27122  mpodvdsmulf1o  27177  dvdsmulf1o  27179  dchrelbas4  27227  dchrinv  27245  2sqlem6  27407  chpo1ubb  27465  dchrmusumlema  27477  dchrisum0lema  27498  ostth3  27622  ltsrec  27814  lrrecfr  27956  addsuniflem  28014  addbday  28031  negsunif  28068  n0fincut  28368  bdayfinbndlem1  28480  elreno2  28508  tgcgr4  28621  eqeelen  28995  brbtwn2  28996  colinearalg  29001  axcgrid  29007  axsegconlem1  29008  ax5seglem4  29023  ax5seglem5  29024  axbtwnid  29030  axpasch  29032  axeuclidlem  29053  axcontlem2  29056  axcontlem4  29058  axcontlem7  29061  axcontlem12  29066  elntg2  29076  isuvtx  29486  uvtx2vtx1edg  29489  uvtx2vtx1edgb  29490  iscplgrnb  29507  iscplgredg  29508  vdiscusgrb  29622  uhgrvd00  29626  upgriswlk  29732  wwlksnext  29984  clwwlkinwwlk  30133  clwwlkel  30139  clwwlkf  30140  clwwlkwwlksb  30147  wwlksext2clwwlk  30150  wwlksubclwwlk  30151  clwwlknonex2lem2  30201  nmounbi  30870  blocnilem  30898  isph  30916  phoeqi  30951  h2hcau  31073  h2hlm  31074  hial2eq2  31201  hoeq1  31924  hoeq2  31925  adjsym  31927  cnvadj  31986  hhcno  31998  hhcnf  31999  adjvalval  32031  leop2  32218  leoptri  32230  mdbr2  32390  dmdbr2  32397  mddmd2  32403  cdj3lem3b  32534  infxrge0gelb  32863  prodindf  32961  toslublem  33071  tosglblem  33073  mgccnv  33098  cntrval2  33271  submarchi  33286  isarchi3  33287  lindfpropd  33481  opprlidlabs  33584  ply1moneq  33687  psrmonmul  33733  cmpcref  34034  lmdvg  34137  eulerpartlemd  34550  subfacp1lem3  35404  subfacp1lem5  35406  satfv1lem  35584  dfrdg2  36015  opnrebl  36542  poimirlem23  37923  broucube  37934  itg2gt0cn  37955  ftc1cnnc  37972  lmclim2  38038  caures  38040  sstotbnd2  38054  rrnmet  38109  rrncmslem  38112  isdrngo3  38239  isidlc  38295  cvrval2  39679  isat3  39712  iscvlat2N  39729  glbconN  39782  ltrneq  40554  cdlemefrs29clN  40804  cdlemefrs32fva  40805  cdleme32fva  40842  cdlemk33N  41314  cdlemk34  41315  cdlemkid3N  41338  cdlemkid4  41339  diaglbN  41460  dibglbN  41571  dihglbcpreN  41705  dihglblem6  41745  hdmap1eulem  42227  hdmap1eulemOLDN  42228  hdmapoc  42336  hlhilocv  42362  primrootsunit1  42496  sn-sup3d  42891  fimgmcyc  42933  wepwsolem  43428  fnwe2lem2  43437  islnm2  43464  onmaxnelsup  43609  onsupnmax  43614  onsupuni  43615  onsupmaxb  43625  onsupeqnmax  43633  iscard5  43921  alephiso2  43943  clsk3nimkb  44425  ntrclsneine0  44450  ntrneineine0  44472  ntrneineine1  44473  ntrneicls00  44474  ntrneicls11  44475  ntrneiiso  44476  ntrneik2  44477  ntrneix2  44478  ntrneikb  44479  ntrneixb  44480  ntrneik3  44481  ntrneix3  44482  ntrneik13  44483  ntrneix13  44484  ntrneik4w  44485  ntrneik4  44486  caofcan  44708  modelac8prim  45377  infxrbnd2  45756  supminfxr  45851  rexanuz2nf  45879  evthiccabs  45885  ellimcabssub0  46006  climf  46011  clim2f  46023  clim2cf  46037  clim0cf  46041  limsupmnflem  46107  limsupre2lem  46111  limsupreuzmpt  46126  supcnvlimsup  46127  limsupge  46148  liminfreuzlem  46189  liminfltlem  46191  liminflimsupclim  46194  liminfpnfuz  46203  xlimpnfxnegmnf2  46245  fourierdlem70  46563  fourierdlem71  46564  fourierdlem73  46566  fourierdlem80  46573  fourierdlem83  46576  fourierdlem87  46580  voliunsge0lem  46859  meaiuninclem  46867  meaiuninc3v  46871  hoidmv1lelem3  46980  hoidmvlelem4  46985  hoidmvlelem5  46986  issmflem  47114  chnerlem1  47269  cfsetsnfsetf  47447  cfsetsnfsetfo  47449  requad2  48012  isubgrgrim  48318  grlicref  48401  islinindfis  48838  elbigolo1  48946  line2x  49143  itscnhlinecirc02p  49174  iscnrm3lem1  49322  ipolublem  49374  ipoglblem  49377  oppcup  49595  uptrlem3  49600  initopropd  49631  termopropd  49632  isinito2lem  49886  termc2  49906  lanup  50029  ranup  50030  aacllem  50189