Theorem ralbidva 3192

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 815	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜒)))
3	2	ralbidv2 3190	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  ralbidv  3194  2ralbidva  3233  raleqbidva  3335  poinxp  5743  soinxp  5744  frinxp  5745  ordunisssuc  6470  fnmptfvd  7037  funimass3  7050  fnnfpeq0  7177  cocan1  7290  cocan2  7291  isores2  7332  isoini2  7338  ofrfvalg  7683  ofrfval2  7696  caofidlcan  7713  tfindsg2  7858  f1oweALT  7969  fnsuppres  8187  dfsmo2  8334  smores  8339  smores2  8341  dfrecs3  8359  naddunif  8680  ac6sfi  9244  fimaxg  9247  ordunifi  9250  isfinite2  9258  fipreima  9315  supisolem  9434  fiming  9460  infempty  9469  ordiso2  9477  ordtypelem7  9486  cantnf  9662  wemapwe  9666  rankval3b  9798  rankonidlem  9800  iscard  9961  acndom  10035  dfac12lem3  10129  kmlem2  10135  cflim2  10247  cfsmolem  10254  ttukeylem6  10498  alephreg  10567  suplem2pr  11038  axsup  11285  sup3  12172  infm3  12174  suprleub  12181  dfinfre  12196  infregelb  12199  ofsubeq0  12215  ofsubge0  12217  zextlt  12670  prime  12677  suprfinzcl  12710  indstr  12940  supxr2  13340  supxrbnd1  13347  supxrbnd2  13348  supxrleub  13352  supxrbnd  13354  infxrgelb  13362  fzshftral  13643  mptnn0fsupp  14033  swrdspsleq  14703  pfxeq  14733  clim  15545  rlim  15546  clim2  15555  clim2c  15556  clim0c  15558  ello1mpt  15572  lo1o1  15583  o1lo1  15588  climabs0  15636  o1compt  15638  rlimdiv  15697  geomulcvg  15930  mertenslem2  15939  mertens  15940  rpnnen2lem12  16281  sqrt2irr  16305  fprodfvdvdsd  16392  fproddvdsd  16393  dfgcd2  16604  isprm7  16767  pc11  16940  pcz  16941  1arith  16987  vdwlem8  17048  vdwlem11  17051  vdw  17054  ramval  17068  pwsle  17546  mrieqvd  17694  mreacs  17714  cidpropd  17766  ismon2  17791  monpropd  17794  isepi  17797  isepi2  17798  subsubc  17910  funcres2b  17954  funcpropd  17959  isfull2  17970  isfth2  17974  fucsect  18032  fucinv  18033  pospropd  18381  ipodrsfi  18595  tsrss  18645  grpidpropd  18720  sgrppropd  18789  mndpropd  18817  smndex1mnd  18972  grppropd  19018  issubg4  19212  gass  19371  gsmsymgrfixlem1  19497  gsmsymgreqlem2  19501  gexdvds  19654  gexdvds2  19655  subgpgp  19667  sylow3lem6  19702  efgval2  19794  efgsp1  19807  dprdf11  20095  subgdmdprd  20106  rngpropd  20252  ringpropd  20371  abvpropd  20916  lsspropd  21116  lbspropd  21198  isridlrng  21322  isridl  21362  phlpropd  21774  ishil2  21838  frlmplusgvalb  21888  frlmvscavalb  21889  frlmvplusgscavalb  21890  lindfmm  21946  islindf4  21957  islindf5  21958  assapropd  21990  psrbaglefi  22045  psrbagconf1o  22048  gsumbagdiaglem  22050  mplmonmul  22156  gsumply1eq  22438  scmatf1  22657  cpmatmcllem  22844  cpmatmcl  22845  decpmataa0  22894  decpmatmulsumfsupp  22899  pmatcollpw2lem  22903  pm2mpmhmlem1  22944  tgss2  23113  isclo  23213  neips  23239  opnnei  23246  isperf3  23279  ssidcn  23381  lmbrf  23386  cnnei  23408  cnrest2  23412  lmss  23424  lmres  23426  ist1-2  23473  ist1-3  23475  isreg2  23503  cmpfi  23534  bwth  23536  1stccn  23589  subislly  23607  kgencn  23682  ptclsg  23741  ptcnplem  23747  xkococnlem  23785  xkoinjcn  23813  tgqtop  23838  qtopcn  23840  fbflim  24102  flimrest  24109  flfnei  24117  isflf  24119  cnflf  24128  fclsopn  24140  fclsbas  24147  fclsrest  24150  isfcf  24160  cnfcf  24168  ptcmplem3  24180  tmdgsum2  24222  eltsms  24259  tsmsgsum  24265  tsmssubm  24269  tsmsf1o  24271  utopsnneiplem  24373  ismet2  24459  prdsxmetlem  24494  elmopn2  24571  prdsbl  24617  metss  24634  metrest  24650  metcnp  24667  metcnp2  24668  metcn  24669  metucn  24697  nrginvrcn  24818  metdsge  24976  divcn  24996  elcncf2  25018  mulc1cncf  25033  cncfmet  25037  evth2  25088  lmmbr2  25387  lmmbrf  25390  iscfil2  25394  cfil3i  25397  iscau2  25405  iscau4  25407  iscauf  25408  caucfil  25411  iscmet3lem3  25418  cfilres  25424  causs  25426  lmclim  25431  rrxmet  25536  evthicc2  25588  cniccbdd  25589  ovolfioo  25595  ovolficc  25596  ismbl2  25655  mbfsup  25792  mbfinf  25793  mbflimsup  25794  0plef  25800  mbfi1flim  25851  xrge0f  25859  itg2mulclem  25874  itgeqa  25942  ellimc2  26005  ellimc3  26007  limcflf  26009  cnlimc  26016  dvferm1  26113  dvferm2  26115  rolle  26118  dvivthlem1  26136  ftc1lem6  26169  itgsubst  26177  mdegle0  26203  deg1leb  26221  plydivex  26427  ulm2  26514  ulmcaulem  26523  ulmcau  26524  ulmdvlem3  26531  abelthlem9  26569  abelth  26570  rlimcnp  27096  ftalem3  27205  issqf  27266  sqf11  27269  mpodvdsmulf1o  27324  dvdsmulf1o  27326  dchrelbas4  27373  dchrinv  27391  2sqlem6  27553  chpo1ubb  27611  dchrmusumlema  27623  dchrisum0lema  27644  ostth3  27768  ltsrec  27960  lrrecfr  28102  addsuniflem  28160  addbday  28177  negsunif  28214  n0fincut  28514  bdayfinbndlem1  28626  elreno2  28654  tgcgr4  28766  eqeelen  29195  brbtwn2  29196  colinearalg  29201  axcgrid  29207  axsegconlem1  29208  ax5seglem4  29223  ax5seglem5  29224  axbtwnid  29230  axpasch  29232  axeuclidlem  29253  axcontlem2  29256  axcontlem4  29258  axcontlem7  29261  axcontlem12  29266  elntg2  29276  isuvtx  29686  uvtx2vtx1edg  29689  uvtx2vtx1edgb  29690  iscplgrnb  29707  iscplgredg  29708  vdiscusgrb  29821  uhgrvd00  29825  upgriswlk  29931  wwlksnext  30183  clwwlkinwwlk  30332  clwwlkel  30338  clwwlkf  30339  clwwlkwwlksb  30346  wwlksext2clwwlk  30349  wwlksubclwwlk  30350  clwwlknonex2lem2  30400  nmounbi  31069  blocnilem  31097  isph  31115  phoeqi  31150  h2hcau  31272  h2hlm  31273  hial2eq2  31400  hoeq1  32123  hoeq2  32124  adjsym  32126  cnvadj  32185  hhcno  32197  hhcnf  32198  adjvalval  32230  leop2  32417  leoptri  32429  mdbr2  32589  dmdbr2  32596  mddmd2  32602  cdj3lem3b  32733  infxrge0gelb  33052  prodindf  33123  toslublem  33233  tosglblem  33235  mgccnv  33260  cntrval2  33432  submarchi  33447  isarchi3  33448  lindfpropd  33639  opprlidlabs  33712  ply1moneq  33823  psrmonmul  33885  cmpcref  34185  lmdvg  34288  eulerpartlemd  34701  subfacp1lem3  35607  subfacp1lem5  35609  satfv1lem  35787  dfrdg2  36218  opnrebl  36754  poimirlem23  38217  broucube  38228  itg2gt0cn  38249  ftc1cnnc  38266  lmclim2  38332  caures  38334  sstotbnd2  38348  rrnmet  38403  rrncmslem  38406  isdrngo3  38533  isidlc  38589  cvrval2  39973  isat3  40006  iscvlat2N  40023  glbconN  40076  ltrneq  40848  cdlemefrs29clN  41098  cdlemefrs32fva  41099  cdleme32fva  41136  cdlemk33N  41608  cdlemk34  41609  cdlemkid3N  41632  cdlemkid4  41633  diaglbN  41754  dibglbN  41865  dihglbcpreN  41999  dihglblem6  42039  hdmap1eulem  42521  hdmap1eulemOLDN  42522  hdmapoc  42630  hlhilocv  42656  primrootsunit1  42789  sn-sup3d  43191  fimgmcyc  43229  wepwsolem  43696  fnwe2lem2  43705  islnm2  43732  onmaxnelsup  43877  onsupnmax  43882  onsupuni  43883  onsupmaxb  43893  onsupeqnmax  43901  iscard5  44189  alephiso2  44211  clsk3nimkb  44693  ntrclsneine0  44718  ntrneineine0  44740  ntrneineine1  44741  ntrneicls00  44742  ntrneicls11  44743  ntrneiiso  44744  ntrneik2  44745  ntrneix2  44746  ntrneikb  44747  ntrneixb  44748  ntrneik3  44749  ntrneix3  44750  ntrneik13  44751  ntrneix13  44752  ntrneik4w  44753  ntrneik4  44754  caofcan  44960  modelac8prim  45628  infxrbnd2  46011  supminfxr  46105  rexanuz2nf  46133  evthiccabs  46139  ellimcabssub0  46260  climf  46265  clim2f  46277  clim2cf  46291  clim0cf  46295  limsupmnflem  46361  limsupre2lem  46365  limsupreuzmpt  46380  supcnvlimsup  46381  limsupge  46402  liminfreuzlem  46443  liminfltlem  46445  liminflimsupclim  46448  liminfpnfuz  46457  xlimpnfxnegmnf2  46499  fourierdlem70  46817  fourierdlem71  46818  fourierdlem73  46820  fourierdlem80  46827  fourierdlem83  46830  fourierdlem87  46834  voliunsge0lem  47113  meaiuninclem  47121  meaiuninc3v  47125  hoidmv1lelem3  47234  hoidmvlelem4  47239  hoidmvlelem5  47240  issmflem  47368  chnerlem1  47525  cfsetsnfsetf  47719  cfsetsnfsetfo  47721  nprmmul1  48200  requad2  48312  isubgrgrim  48618  grlicref  48701  islinindfis  49149  elbigolo1  49257  line2x  49454  itscnhlinecirc02p  49485  iscnrm3lem1  49632  ipolublem  49684  ipoglblem  49687  oppcup  49905  uptrlem3  49910  initopropd  49941  termopropd  49942  isinito2lem  50196  termc2  50216  lanup  50339  ranup  50340  aacllem  50510