Theorem ralbidva 3153

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

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

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 207  df-an 396  df-ral 3048

This theorem is referenced by:  ralbidv  3155  2ralbidva  3194  raleqbidva  3298  poinxp  5695  soinxp  5696  frinxp  5697  ordunisssuc  6414  fnmptfvd  6974  funimass3  6987  fnnfpeq0  7112  cocan1  7225  cocan2  7226  isores2  7267  isoini2  7273  ofrfvalg  7618  ofrfval2  7631  caofidlcan  7648  tfindsg2  7792  f1oweALT  7904  fnsuppres  8121  dfsmo2  8267  smores  8272  smores2  8274  dfrecs3  8292  naddunif  8608  ac6sfi  9168  fimaxg  9171  ordunifi  9174  isfinite2  9182  fipreima  9242  supisolem  9358  fiming  9384  infempty  9393  ordiso2  9401  ordtypelem7  9410  cantnf  9583  wemapwe  9587  rankval3b  9719  rankonidlem  9721  iscard  9868  acndom  9942  dfac12lem3  10037  kmlem2  10043  cflim2  10154  cfsmolem  10161  ttukeylem6  10405  alephreg  10473  suplem2pr  10944  axsup  11188  sup3  12079  infm3  12081  suprleub  12088  dfinfre  12103  infregelb  12106  ofsubeq0  12122  ofsubge0  12124  zextlt  12547  prime  12554  suprfinzcl  12587  indstr  12814  supxr2  13213  supxrbnd1  13220  supxrbnd2  13221  supxrleub  13225  supxrbnd  13227  infxrgelb  13235  fzshftral  13515  mptnn0fsupp  13904  swrdspsleq  14573  pfxeq  14603  clim  15401  rlim  15402  clim2  15411  clim2c  15412  clim0c  15414  ello1mpt  15428  lo1o1  15439  o1lo1  15444  climabs0  15492  o1compt  15494  rlimdiv  15553  geomulcvg  15783  mertenslem2  15792  mertens  15793  rpnnen2lem12  16134  sqrt2irr  16158  fprodfvdvdsd  16245  fproddvdsd  16246  dfgcd2  16457  isprm7  16619  pc11  16792  pcz  16793  1arith  16839  vdwlem8  16900  vdwlem11  16903  vdw  16906  ramval  16920  pwsle  17396  mrieqvd  17544  mreacs  17564  cidpropd  17616  ismon2  17641  monpropd  17644  isepi  17647  isepi2  17648  subsubc  17760  funcres2b  17804  funcpropd  17809  isfull2  17820  isfth2  17824  fucsect  17882  fucinv  17883  pospropd  18231  ipodrsfi  18445  tsrss  18495  grpidpropd  18570  sgrppropd  18639  mndpropd  18667  smndex1mnd  18818  grppropd  18864  issubg4  19058  gass  19213  gsmsymgrfixlem1  19339  gsmsymgreqlem2  19343  gexdvds  19496  gexdvds2  19497  subgpgp  19509  sylow3lem6  19544  efgval2  19636  efgsp1  19649  dprdf11  19937  subgdmdprd  19948  rngpropd  20092  ringpropd  20206  abvpropd  20750  lsspropd  20951  lbspropd  21033  isridlrng  21156  isridl  21189  phlpropd  21592  ishil2  21656  frlmplusgvalb  21706  frlmvscavalb  21707  frlmvplusgscavalb  21708  lindfmm  21764  islindf4  21775  islindf5  21776  assapropd  21809  psrbaglefi  21863  psrbagconf1o  21866  gsumbagdiaglem  21867  mplmonmul  21971  gsumply1eq  22224  scmatf1  22446  cpmatmcllem  22633  cpmatmcl  22634  decpmataa0  22683  decpmatmulsumfsupp  22688  pmatcollpw2lem  22692  pm2mpmhmlem1  22733  tgss2  22902  isclo  23002  neips  23028  opnnei  23035  isperf3  23068  ssidcn  23170  lmbrf  23175  cnnei  23197  cnrest2  23201  lmss  23213  lmres  23215  ist1-2  23262  ist1-3  23264  isreg2  23292  cmpfi  23323  bwth  23325  1stccn  23378  subislly  23396  kgencn  23471  ptclsg  23530  ptcnplem  23536  xkococnlem  23574  xkoinjcn  23602  tgqtop  23627  qtopcn  23629  fbflim  23891  flimrest  23898  flfnei  23906  isflf  23908  cnflf  23917  fclsopn  23929  fclsbas  23936  fclsrest  23939  isfcf  23949  cnfcf  23957  ptcmplem3  23969  tmdgsum2  24011  eltsms  24048  tsmsgsum  24054  tsmssubm  24058  tsmsf1o  24060  utopsnneiplem  24162  ismet2  24248  prdsxmetlem  24283  elmopn2  24360  prdsbl  24406  metss  24423  metrest  24439  metcnp  24456  metcnp2  24457  metcn  24458  metucn  24486  nrginvrcn  24607  metdsge  24765  divcnOLD  24784  divcn  24786  elcncf2  24810  mulc1cncf  24825  cncfmet  24829  evth2  24886  lmmbr2  25186  lmmbrf  25189  iscfil2  25193  cfil3i  25196  iscau2  25204  iscau4  25206  iscauf  25207  caucfil  25210  iscmet3lem3  25217  cfilres  25223  causs  25225  lmclim  25230  rrxmet  25335  evthicc2  25388  cniccbdd  25389  ovolfioo  25395  ovolficc  25396  ismbl2  25455  mbfsup  25592  mbfinf  25593  mbflimsup  25594  0plef  25600  mbfi1flim  25651  xrge0f  25659  itg2mulclem  25674  itgeqa  25742  ellimc2  25805  ellimc3  25807  limcflf  25809  cnlimc  25816  dvferm1  25916  dvferm2  25918  rolle  25921  dvivthlem1  25940  ftc1lem6  25975  itgsubst  25983  mdegle0  26009  deg1leb  26027  plydivex  26232  ulm2  26321  ulmcaulem  26330  ulmcau  26331  ulmdvlem3  26338  abelthlem9  26377  abelth  26378  rlimcnp  26902  ftalem3  27012  issqf  27073  sqf11  27076  mpodvdsmulf1o  27131  dvdsmulf1o  27133  dchrelbas4  27181  dchrinv  27199  2sqlem6  27361  chpo1ubb  27419  dchrmusumlema  27431  dchrisum0lema  27452  ostth3  27576  sltrec  27762  lrrecfr  27886  addsuniflem  27944  addsbday  27960  negsunif  27997  n0sfincut  28282  tgcgr4  28509  eqeelen  28882  brbtwn2  28883  colinearalg  28888  axcgrid  28894  axsegconlem1  28895  ax5seglem4  28910  ax5seglem5  28911  axbtwnid  28917  axpasch  28919  axeuclidlem  28940  axcontlem2  28943  axcontlem4  28945  axcontlem7  28948  axcontlem12  28953  elntg2  28963  isuvtx  29373  uvtx2vtx1edg  29376  uvtx2vtx1edgb  29377  iscplgrnb  29394  iscplgredg  29395  vdiscusgrb  29509  uhgrvd00  29513  upgriswlk  29619  wwlksnext  29871  clwwlkinwwlk  30020  clwwlkel  30026  clwwlkf  30027  clwwlkwwlksb  30034  wwlksext2clwwlk  30037  wwlksubclwwlk  30038  clwwlknonex2lem2  30088  nmounbi  30756  blocnilem  30784  isph  30802  phoeqi  30837  h2hcau  30959  h2hlm  30960  hial2eq2  31087  hoeq1  31810  hoeq2  31811  adjsym  31813  cnvadj  31872  hhcno  31884  hhcnf  31885  adjvalval  31917  leop2  32104  leoptri  32116  mdbr2  32276  dmdbr2  32283  mddmd2  32289  cdj3lem3b  32420  infxrge0gelb  32749  prodindf  32844  toslublem  32953  tosglblem  32955  mgccnv  32980  cntrval2  33140  submarchi  33155  isarchi3  33156  lindfpropd  33347  opprlidlabs  33450  ply1moneq  33550  cmpcref  33863  lmdvg  33966  eulerpartlemd  34379  subfacp1lem3  35226  subfacp1lem5  35228  satfv1lem  35406  dfrdg2  35837  opnrebl  36364  poimirlem23  37682  broucube  37693  itg2gt0cn  37714  ftc1cnnc  37731  lmclim2  37797  caures  37799  sstotbnd2  37813  rrnmet  37868  rrncmslem  37871  isdrngo3  37998  isidlc  38054  cvrval2  39372  isat3  39405  iscvlat2N  39422  glbconN  39475  ltrneq  40247  cdlemefrs29clN  40497  cdlemefrs32fva  40498  cdleme32fva  40535  cdlemk33N  41007  cdlemk34  41008  cdlemkid3N  41031  cdlemkid4  41032  diaglbN  41153  dibglbN  41264  dihglbcpreN  41398  dihglblem6  41438  hdmap1eulem  41920  hdmap1eulemOLDN  41921  hdmapoc  42029  hlhilocv  42055  primrootsunit1  42189  sn-sup3d  42584  fimgmcyc  42626  wepwsolem  43134  fnwe2lem2  43143  islnm2  43170  onmaxnelsup  43315  onsupnmax  43320  onsupuni  43321  onsupmaxb  43331  onsupeqnmax  43339  iscard5  43628  alephiso2  43650  clsk3nimkb  44132  ntrclsneine0  44157  ntrneineine0  44179  ntrneineine1  44180  ntrneicls00  44181  ntrneicls11  44182  ntrneiiso  44183  ntrneik2  44184  ntrneix2  44185  ntrneikb  44186  ntrneixb  44187  ntrneik3  44188  ntrneix3  44189  ntrneik13  44190  ntrneix13  44191  ntrneik4w  44192  ntrneik4  44193  caofcan  44415  modelac8prim  45084  infxrbnd2  45466  supminfxr  45561  rexanuz2nf  45589  evthiccabs  45595  ellimcabssub0  45716  climf  45721  clim2f  45733  clim2cf  45747  clim0cf  45751  limsupmnflem  45817  limsupre2lem  45821  limsupreuzmpt  45836  supcnvlimsup  45837  limsupge  45858  liminfreuzlem  45899  liminfltlem  45901  liminflimsupclim  45904  liminfpnfuz  45913  xlimpnfxnegmnf2  45955  fourierdlem70  46273  fourierdlem71  46274  fourierdlem73  46276  fourierdlem80  46283  fourierdlem83  46286  fourierdlem87  46290  voliunsge0lem  46569  meaiuninclem  46577  meaiuninc3v  46581  hoidmv1lelem3  46690  hoidmvlelem4  46695  hoidmvlelem5  46696  issmflem  46824  chnerlem1  46979  cfsetsnfsetf  47157  cfsetsnfsetfo  47159  requad2  47722  isubgrgrim  48028  grlicref  48111  islinindfis  48549  elbigolo1  48657  line2x  48854  itscnhlinecirc02p  48885  iscnrm3lem1  49033  ipolublem  49085  ipoglblem  49088  oppcup  49307  uptrlem3  49312  initopropd  49343  termopropd  49344  isinito2lem  49598  termc2  49618  lanup  49741  ranup  49742  aacllem  49901