Theorem ralbidva 3154

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

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

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 3045

This theorem is referenced by:  ralbidv  3156  2ralbidva  3199  raleqbidva  3305  poinxp  5719  soinxp  5720  frinxp  5721  ordunisssuc  6440  fnmptfvd  7013  funimass3  7026  fnnfpeq0  7152  cocan1  7266  cocan2  7267  isores2  7308  isoini2  7314  ofrfvalg  7661  ofrfval2  7674  caofidlcan  7691  tfindsg2  7838  f1oweALT  7951  fnsuppres  8170  dfsmo2  8316  smores  8321  smores2  8323  dfrecs3  8341  naddunif  8657  ac6sfi  9231  fimaxg  9234  ordunifi  9237  isfinite2  9245  fipreima  9309  supisolem  9425  fiming  9451  infempty  9460  ordiso2  9468  ordtypelem7  9477  cantnf  9646  wemapwe  9650  rankval3b  9779  rankonidlem  9781  iscard  9928  acndom  10004  dfac12lem3  10099  kmlem2  10105  cflim2  10216  cfsmolem  10223  ttukeylem6  10467  alephreg  10535  suplem2pr  11006  axsup  11249  sup3  12140  infm3  12142  suprleub  12149  dfinfre  12164  infregelb  12167  ofsubeq0  12183  ofsubge0  12185  zextlt  12608  prime  12615  suprfinzcl  12648  indstr  12875  supxr2  13274  supxrbnd1  13281  supxrbnd2  13282  supxrleub  13286  supxrbnd  13288  infxrgelb  13296  fzshftral  13576  mptnn0fsupp  13962  swrdspsleq  14630  pfxeq  14661  clim  15460  rlim  15461  clim2  15470  clim2c  15471  clim0c  15473  ello1mpt  15487  lo1o1  15498  o1lo1  15503  climabs0  15551  o1compt  15553  rlimdiv  15612  geomulcvg  15842  mertenslem2  15851  mertens  15852  rpnnen2lem12  16193  sqrt2irr  16217  fprodfvdvdsd  16304  fproddvdsd  16305  dfgcd2  16516  isprm7  16678  pc11  16851  pcz  16852  1arith  16898  vdwlem8  16959  vdwlem11  16962  vdw  16965  ramval  16979  pwsle  17455  mrieqvd  17599  mreacs  17619  cidpropd  17671  ismon2  17696  monpropd  17699  isepi  17702  isepi2  17703  subsubc  17815  funcres2b  17859  funcpropd  17864  isfull2  17875  isfth2  17879  fucsect  17937  fucinv  17938  pospropd  18286  ipodrsfi  18498  tsrss  18548  grpidpropd  18589  sgrppropd  18658  mndpropd  18686  smndex1mnd  18837  grppropd  18883  issubg4  19077  gass  19233  gsmsymgrfixlem1  19357  gsmsymgreqlem2  19361  gexdvds  19514  gexdvds2  19515  subgpgp  19527  sylow3lem6  19562  efgval2  19654  efgsp1  19667  dprdf11  19955  subgdmdprd  19966  rngpropd  20083  ringpropd  20197  abvpropd  20744  lsspropd  20924  lbspropd  21006  isridlrng  21129  isridl  21162  phlpropd  21564  ishil2  21628  frlmplusgvalb  21678  frlmvscavalb  21679  frlmvplusgscavalb  21680  lindfmm  21736  islindf4  21747  islindf5  21748  assapropd  21781  psrbaglefi  21835  psrbagconf1o  21838  gsumbagdiaglem  21839  mplmonmul  21943  gsumply1eq  22196  scmatf1  22418  cpmatmcllem  22605  cpmatmcl  22606  decpmataa0  22655  decpmatmulsumfsupp  22660  pmatcollpw2lem  22664  pm2mpmhmlem1  22705  tgss2  22874  isclo  22974  neips  23000  opnnei  23007  isperf3  23040  ssidcn  23142  lmbrf  23147  cnnei  23169  cnrest2  23173  lmss  23185  lmres  23187  ist1-2  23234  ist1-3  23236  isreg2  23264  cmpfi  23295  bwth  23297  1stccn  23350  subislly  23368  kgencn  23443  ptclsg  23502  ptcnplem  23508  xkococnlem  23546  xkoinjcn  23574  tgqtop  23599  qtopcn  23601  fbflim  23863  flimrest  23870  flfnei  23878  isflf  23880  cnflf  23889  fclsopn  23901  fclsbas  23908  fclsrest  23911  isfcf  23921  cnfcf  23929  ptcmplem3  23941  tmdgsum2  23983  eltsms  24020  tsmsgsum  24026  tsmssubm  24030  tsmsf1o  24032  utopsnneiplem  24135  ismet2  24221  prdsxmetlem  24256  elmopn2  24333  prdsbl  24379  metss  24396  metrest  24412  metcnp  24429  metcnp2  24430  metcn  24431  metucn  24459  nrginvrcn  24580  metdsge  24738  divcnOLD  24757  divcn  24759  elcncf2  24783  mulc1cncf  24798  cncfmet  24802  evth2  24859  lmmbr2  25159  lmmbrf  25162  iscfil2  25166  cfil3i  25169  iscau2  25177  iscau4  25179  iscauf  25180  caucfil  25183  iscmet3lem3  25190  cfilres  25196  causs  25198  lmclim  25203  rrxmet  25308  evthicc2  25361  cniccbdd  25362  ovolfioo  25368  ovolficc  25369  ismbl2  25428  mbfsup  25565  mbfinf  25566  mbflimsup  25567  0plef  25573  mbfi1flim  25624  xrge0f  25632  itg2mulclem  25647  itgeqa  25715  ellimc2  25778  ellimc3  25780  limcflf  25782  cnlimc  25789  dvferm1  25889  dvferm2  25891  rolle  25894  dvivthlem1  25913  ftc1lem6  25948  itgsubst  25956  mdegle0  25982  deg1leb  26000  plydivex  26205  ulm2  26294  ulmcaulem  26303  ulmcau  26304  ulmdvlem3  26311  abelthlem9  26350  abelth  26351  rlimcnp  26875  ftalem3  26985  issqf  27046  sqf11  27049  mpodvdsmulf1o  27104  dvdsmulf1o  27106  dchrelbas4  27154  dchrinv  27172  2sqlem6  27334  chpo1ubb  27392  dchrmusumlema  27404  dchrisum0lema  27425  ostth3  27549  sltrec  27732  lrrecfr  27850  addsuniflem  27908  addsbday  27924  negsunif  27961  n0sfincut  28246  tgcgr4  28458  eqeelen  28831  brbtwn2  28832  colinearalg  28837  axcgrid  28843  axsegconlem1  28844  ax5seglem4  28859  ax5seglem5  28860  axbtwnid  28866  axpasch  28868  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem12  28902  elntg2  28912  isuvtx  29322  uvtx2vtx1edg  29325  uvtx2vtx1edgb  29326  iscplgrnb  29343  iscplgredg  29344  vdiscusgrb  29458  uhgrvd00  29462  upgriswlk  29569  wwlksnext  29823  clwwlkinwwlk  29969  clwwlkel  29975  clwwlkf  29976  clwwlkwwlksb  29983  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  clwwlknonex2lem2  30037  nmounbi  30705  blocnilem  30733  isph  30751  phoeqi  30786  h2hcau  30908  h2hlm  30909  hial2eq2  31036  hoeq1  31759  hoeq2  31760  adjsym  31762  cnvadj  31821  hhcno  31833  hhcnf  31834  adjvalval  31866  leop2  32053  leoptri  32065  mdbr2  32225  dmdbr2  32232  mddmd2  32238  cdj3lem3b  32369  infxrge0gelb  32689  prodindf  32786  toslublem  32898  tosglblem  32900  mgccnv  32925  cntrval2  33128  submarchi  33140  isarchi3  33141  lindfpropd  33353  opprlidlabs  33456  ply1moneq  33555  cmpcref  33840  lmdvg  33943  eulerpartlemd  34357  subfacp1lem3  35169  subfacp1lem5  35171  satfv1lem  35349  dfrdg2  35783  opnrebl  36308  poimirlem23  37637  broucube  37648  itg2gt0cn  37669  ftc1cnnc  37686  lmclim2  37752  caures  37754  sstotbnd2  37768  rrnmet  37823  rrncmslem  37826  isdrngo3  37953  isidlc  38009  cvrval2  39267  isat3  39300  iscvlat2N  39317  glbconN  39370  glbconNOLD  39371  ltrneq  40143  cdlemefrs29clN  40393  cdlemefrs32fva  40394  cdleme32fva  40431  cdlemk33N  40903  cdlemk34  40904  cdlemkid3N  40927  cdlemkid4  40928  diaglbN  41049  dibglbN  41160  dihglbcpreN  41294  dihglblem6  41334  hdmap1eulem  41816  hdmap1eulemOLDN  41817  hdmapoc  41925  hlhilocv  41951  primrootsunit1  42085  sn-sup3d  42480  fimgmcyc  42522  wepwsolem  43031  fnwe2lem2  43040  islnm2  43067  onmaxnelsup  43212  onsupnmax  43217  onsupuni  43218  onsupmaxb  43228  onsupeqnmax  43236  iscard5  43525  alephiso2  43547  clsk3nimkb  44029  ntrclsneine0  44054  ntrneineine0  44076  ntrneineine1  44077  ntrneicls00  44078  ntrneicls11  44079  ntrneiiso  44080  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  ntrneik4w  44089  ntrneik4  44090  caofcan  44312  modelac8prim  44982  infxrbnd2  45365  supminfxr  45460  rexanuz2nf  45488  evthiccabs  45494  ellimcabssub0  45615  climf  45620  clim2f  45634  clim2cf  45648  clim0cf  45652  limsupmnflem  45718  limsupre2lem  45722  limsupreuzmpt  45737  supcnvlimsup  45738  limsupge  45759  liminfreuzlem  45800  liminfltlem  45802  liminflimsupclim  45805  liminfpnfuz  45814  xlimpnfxnegmnf2  45856  fourierdlem70  46174  fourierdlem71  46175  fourierdlem73  46177  fourierdlem80  46184  fourierdlem83  46187  fourierdlem87  46191  voliunsge0lem  46470  meaiuninclem  46478  meaiuninc3v  46482  hoidmv1lelem3  46591  hoidmvlelem4  46596  hoidmvlelem5  46597  issmflem  46725  cfsetsnfsetf  47059  cfsetsnfsetfo  47061  requad2  47624  isubgrgrim  47929  grlicref  48004  islinindfis  48438  elbigolo1  48546  line2x  48743  itscnhlinecirc02p  48774  iscnrm3lem1  48922  ipolublem  48974  ipoglblem  48977  oppcup  49196  uptrlem3  49201  initopropd  49232  termopropd  49233  isinito2lem  49487  termc2  49507  lanup  49630  ranup  49631  aacllem  49790