Theorem ralbidva 3161

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  ralbidv  3163  2ralbidva  3203  raleqbidva  3311  poinxp  5735  soinxp  5736  frinxp  5737  ordunisssuc  6459  fnmptfvd  7030  funimass3  7043  fnnfpeq0  7169  cocan1  7283  cocan2  7284  isores2  7325  isoini2  7331  ofrfvalg  7677  ofrfval2  7690  caofidlcan  7707  tfindsg2  7855  f1oweALT  7969  fnsuppres  8188  dfsmo2  8359  smores  8364  smores2  8366  dfrecs3  8384  dfrecs3OLD  8385  naddunif  8703  ac6sfi  9290  fimaxg  9293  ordunifi  9296  isfinite2  9304  fipreima  9368  supisolem  9484  fiming  9510  infempty  9519  ordiso2  9527  ordtypelem7  9536  cantnf  9705  wemapwe  9709  rankval3b  9838  rankonidlem  9840  iscard  9987  acndom  10063  dfac12lem3  10158  kmlem2  10164  cflim2  10275  cfsmolem  10282  ttukeylem6  10526  alephreg  10594  suplem2pr  11065  axsup  11308  sup3  12197  infm3  12199  suprleub  12206  dfinfre  12221  infregelb  12224  ofsubeq0  12235  ofsubge0  12237  zextlt  12665  prime  12672  suprfinzcl  12705  indstr  12930  supxr2  13328  supxrbnd1  13335  supxrbnd2  13336  supxrleub  13340  supxrbnd  13342  infxrgelb  13350  fzshftral  13630  mptnn0fsupp  14013  swrdspsleq  14681  pfxeq  14712  clim  15508  rlim  15509  clim2  15518  clim2c  15519  clim0c  15521  ello1mpt  15535  lo1o1  15546  o1lo1  15551  climabs0  15599  o1compt  15601  rlimdiv  15660  geomulcvg  15890  mertenslem2  15899  mertens  15900  rpnnen2lem12  16241  sqrt2irr  16265  fprodfvdvdsd  16351  fproddvdsd  16352  dfgcd2  16563  isprm7  16725  pc11  16898  pcz  16899  1arith  16945  vdwlem8  17006  vdwlem11  17009  vdw  17012  ramval  17026  pwsle  17504  mrieqvd  17648  mreacs  17668  cidpropd  17720  ismon2  17745  monpropd  17748  isepi  17751  isepi2  17752  subsubc  17864  funcres2b  17908  funcpropd  17913  isfull2  17924  isfth2  17928  fucsect  17986  fucinv  17987  pospropd  18335  ipodrsfi  18547  tsrss  18597  grpidpropd  18638  sgrppropd  18707  mndpropd  18735  smndex1mnd  18886  grppropd  18932  issubg4  19126  gass  19282  gsmsymgrfixlem1  19406  gsmsymgreqlem2  19410  gexdvds  19563  gexdvds2  19564  subgpgp  19576  sylow3lem6  19611  efgval2  19703  efgsp1  19716  dprdf11  20004  subgdmdprd  20015  rngpropd  20132  ringpropd  20246  abvpropd  20793  lsspropd  20973  lbspropd  21055  isridlrng  21178  isridl  21211  phlpropd  21613  ishil2  21677  frlmplusgvalb  21727  frlmvscavalb  21728  frlmvplusgscavalb  21729  lindfmm  21785  islindf4  21796  islindf5  21797  assapropd  21830  psrbaglefi  21884  psrbagconf1o  21887  gsumbagdiaglem  21888  mplmonmul  21992  gsumply1eq  22245  scmatf1  22467  cpmatmcllem  22654  cpmatmcl  22655  decpmataa0  22704  decpmatmulsumfsupp  22709  pmatcollpw2lem  22713  pm2mpmhmlem1  22754  tgss2  22923  isclo  23023  neips  23049  opnnei  23056  isperf3  23089  ssidcn  23191  lmbrf  23196  cnnei  23218  cnrest2  23222  lmss  23234  lmres  23236  ist1-2  23283  ist1-3  23285  isreg2  23313  cmpfi  23344  bwth  23346  1stccn  23399  subislly  23417  kgencn  23492  ptclsg  23551  ptcnplem  23557  xkococnlem  23595  xkoinjcn  23623  tgqtop  23648  qtopcn  23650  fbflim  23912  flimrest  23919  flfnei  23927  isflf  23929  cnflf  23938  fclsopn  23950  fclsbas  23957  fclsrest  23960  isfcf  23970  cnfcf  23978  ptcmplem3  23990  tmdgsum2  24032  eltsms  24069  tsmsgsum  24075  tsmssubm  24079  tsmsf1o  24081  utopsnneiplem  24184  ismet2  24270  prdsxmetlem  24305  elmopn2  24382  prdsbl  24428  metss  24445  metrest  24461  metcnp  24478  metcnp2  24479  metcn  24480  metucn  24508  nrginvrcn  24629  metdsge  24787  divcnOLD  24806  divcn  24808  elcncf2  24832  mulc1cncf  24847  cncfmet  24851  evth2  24908  lmmbr2  25209  lmmbrf  25212  iscfil2  25216  cfil3i  25219  iscau2  25227  iscau4  25229  iscauf  25230  caucfil  25233  iscmet3lem3  25240  cfilres  25246  causs  25248  lmclim  25253  rrxmet  25358  evthicc2  25411  cniccbdd  25412  ovolfioo  25418  ovolficc  25419  ismbl2  25478  mbfsup  25615  mbfinf  25616  mbflimsup  25617  0plef  25623  mbfi1flim  25674  xrge0f  25682  itg2mulclem  25697  itgeqa  25765  ellimc2  25828  ellimc3  25830  limcflf  25832  cnlimc  25839  dvferm1  25939  dvferm2  25941  rolle  25944  dvivthlem1  25963  ftc1lem6  25998  itgsubst  26006  mdegle0  26032  deg1leb  26050  plydivex  26255  ulm2  26344  ulmcaulem  26353  ulmcau  26354  ulmdvlem3  26361  abelthlem9  26400  abelth  26401  rlimcnp  26925  ftalem3  27035  issqf  27096  sqf11  27099  mpodvdsmulf1o  27154  dvdsmulf1o  27156  dchrelbas4  27204  dchrinv  27222  2sqlem6  27384  chpo1ubb  27442  dchrmusumlema  27454  dchrisum0lema  27475  ostth3  27599  sltrec  27782  lrrecfr  27893  addsuniflem  27951  addsbday  27967  negsunif  28004  tgcgr4  28456  eqeelen  28829  brbtwn2  28830  colinearalg  28835  axcgrid  28841  axsegconlem1  28842  ax5seglem4  28857  ax5seglem5  28858  axbtwnid  28864  axpasch  28866  axeuclidlem  28887  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  axcontlem12  28900  elntg2  28910  isuvtx  29320  uvtx2vtx1edg  29323  uvtx2vtx1edgb  29324  iscplgrnb  29341  iscplgredg  29342  vdiscusgrb  29456  uhgrvd00  29460  upgriswlk  29567  wwlksnext  29821  clwwlkinwwlk  29967  clwwlkel  29973  clwwlkf  29974  clwwlkwwlksb  29981  wwlksext2clwwlk  29984  wwlksubclwwlk  29985  clwwlknonex2lem2  30035  nmounbi  30703  blocnilem  30731  isph  30749  phoeqi  30784  h2hcau  30906  h2hlm  30907  hial2eq2  31034  hoeq1  31757  hoeq2  31758  adjsym  31760  cnvadj  31819  hhcno  31831  hhcnf  31832  adjvalval  31864  leop2  32051  leoptri  32063  mdbr2  32223  dmdbr2  32230  mddmd2  32236  cdj3lem3b  32367  infxrge0gelb  32689  prodindf  32786  toslublem  32898  tosglblem  32900  mgccnv  32925  submarchi  33130  isarchi3  33131  lindfpropd  33343  opprlidlabs  33446  ply1moneq  33545  cmpcref  33827  lmdvg  33930  eulerpartlemd  34344  subfacp1lem3  35150  subfacp1lem5  35152  satfv1lem  35330  dfrdg2  35759  opnrebl  36284  poimirlem23  37613  broucube  37624  itg2gt0cn  37645  ftc1cnnc  37662  lmclim2  37728  caures  37730  sstotbnd2  37744  rrnmet  37799  rrncmslem  37802  isdrngo3  37929  isidlc  37985  cvrval2  39238  isat3  39271  iscvlat2N  39288  glbconN  39341  glbconNOLD  39342  ltrneq  40114  cdlemefrs29clN  40364  cdlemefrs32fva  40365  cdleme32fva  40402  cdlemk33N  40874  cdlemk34  40875  cdlemkid3N  40898  cdlemkid4  40899  diaglbN  41020  dibglbN  41131  dihglbcpreN  41265  dihglblem6  41305  hdmap1eulem  41787  hdmap1eulemOLDN  41788  hdmapoc  41896  hlhilocv  41922  primrootsunit1  42056  sn-sup3d  42462  fimgmcyc  42504  wepwsolem  43013  fnwe2lem2  43022  islnm2  43049  onmaxnelsup  43194  onsupnmax  43199  onsupuni  43200  onsupmaxb  43210  onsupeqnmax  43218  iscard5  43507  alephiso2  43529  clsk3nimkb  44011  ntrclsneine0  44036  ntrneineine0  44058  ntrneineine1  44059  ntrneicls00  44060  ntrneicls11  44061  ntrneiiso  44062  ntrneik2  44063  ntrneix2  44064  ntrneikb  44065  ntrneixb  44066  ntrneik3  44067  ntrneix3  44068  ntrneik13  44069  ntrneix13  44070  ntrneik4w  44071  ntrneik4  44072  caofcan  44295  modelac8prim  44965  infxrbnd2  45344  supminfxr  45439  rexanuz2nf  45467  evthiccabs  45473  ellimcabssub0  45594  climf  45599  clim2f  45613  clim2cf  45627  clim0cf  45631  limsupmnflem  45697  limsupre2lem  45701  limsupreuzmpt  45716  supcnvlimsup  45717  limsupge  45738  liminfreuzlem  45779  liminfltlem  45781  liminflimsupclim  45784  liminfpnfuz  45793  xlimpnfxnegmnf2  45835  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem80  46163  fourierdlem83  46166  fourierdlem87  46170  voliunsge0lem  46449  meaiuninclem  46457  meaiuninc3v  46461  hoidmv1lelem3  46570  hoidmvlelem4  46575  hoidmvlelem5  46576  issmflem  46704  cfsetsnfsetf  47035  cfsetsnfsetfo  47037  requad2  47585  isubgrgrim  47890  grlicref  47965  islinindfis  48373  elbigolo1  48485  line2x  48682  itscnhlinecirc02p  48713  iscnrm3lem1  48856  ipolublem  48908  ipoglblem  48911  oppcup  49088  initopropd  49108  termopropd  49109  isinito2lem  49331  termc2  49351  lanup  49463  ranup  49464  aacllem  49613