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  3302  poinxp  5707  soinxp  5708  frinxp  5709  ordunisssuc  6427  fnmptfvd  6989  funimass3  7002  fnnfpeq0  7128  cocan1  7241  cocan2  7242  isores2  7283  isoini2  7289  ofrfvalg  7634  ofrfval2  7647  caofidlcan  7664  tfindsg2  7808  f1oweALT  7920  fnsuppres  8136  dfsmo2  8282  smores  8287  smores2  8289  dfrecs3  8307  naddunif  8624  ac6sfi  9189  fimaxg  9192  ordunifi  9195  isfinite2  9203  fipreima  9263  supisolem  9382  fiming  9408  infempty  9417  ordiso2  9425  ordtypelem7  9434  cantnf  9609  wemapwe  9613  rankval3b  9745  rankonidlem  9747  iscard  9894  acndom  9968  dfac12lem3  10063  kmlem2  10069  cflim2  10180  cfsmolem  10187  ttukeylem6  10431  alephreg  10500  suplem2pr  10971  axsup  11216  sup3  12108  infm3  12110  suprleub  12117  dfinfre  12132  infregelb  12135  ofsubeq0  12151  ofsubge0  12153  zextlt  12598  prime  12605  suprfinzcl  12638  indstr  12861  supxr2  13261  supxrbnd1  13268  supxrbnd2  13269  supxrleub  13273  supxrbnd  13275  infxrgelb  13283  fzshftral  13564  mptnn0fsupp  13954  swrdspsleq  14623  pfxeq  14653  clim  15451  rlim  15452  clim2  15461  clim2c  15462  clim0c  15464  ello1mpt  15478  lo1o1  15489  o1lo1  15494  climabs0  15542  o1compt  15544  rlimdiv  15603  geomulcvg  15836  mertenslem2  15845  mertens  15846  rpnnen2lem12  16187  sqrt2irr  16211  fprodfvdvdsd  16298  fproddvdsd  16299  dfgcd2  16510  isprm7  16673  pc11  16846  pcz  16847  1arith  16893  vdwlem8  16954  vdwlem11  16957  vdw  16960  ramval  16974  pwsle  17451  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  18500  tsrss  18550  grpidpropd  18625  sgrppropd  18694  mndpropd  18722  smndex1mnd  18876  grppropd  18922  issubg4  19116  gass  19271  gsmsymgrfixlem1  19397  gsmsymgreqlem2  19401  gexdvds  19554  gexdvds2  19555  subgpgp  19567  sylow3lem6  19602  efgval2  19694  efgsp1  19707  dprdf11  19995  subgdmdprd  20006  rngpropd  20150  ringpropd  20264  abvpropd  20807  lsspropd  21008  lbspropd  21090  isridlrng  21213  isridl  21246  phlpropd  21649  ishil2  21713  frlmplusgvalb  21763  frlmvscavalb  21764  frlmvplusgscavalb  21765  lindfmm  21821  islindf4  21832  islindf5  21833  assapropd  21865  psrbaglefi  21920  psrbagconf1o  21923  gsumbagdiaglem  21924  mplmonmul  22028  gsumply1eq  22288  scmatf1  22510  cpmatmcllem  22697  cpmatmcl  22698  decpmataa0  22747  decpmatmulsumfsupp  22752  pmatcollpw2lem  22756  pm2mpmhmlem1  22797  tgss2  22966  isclo  23066  neips  23092  opnnei  23099  isperf3  23132  ssidcn  23234  lmbrf  23239  cnnei  23261  cnrest2  23265  lmss  23277  lmres  23279  ist1-2  23326  ist1-3  23328  isreg2  23356  cmpfi  23387  bwth  23389  1stccn  23442  subislly  23460  kgencn  23535  ptclsg  23594  ptcnplem  23600  xkococnlem  23638  xkoinjcn  23666  tgqtop  23691  qtopcn  23693  fbflim  23955  flimrest  23962  flfnei  23970  isflf  23972  cnflf  23981  fclsopn  23993  fclsbas  24000  fclsrest  24003  isfcf  24013  cnfcf  24021  ptcmplem3  24033  tmdgsum2  24075  eltsms  24112  tsmsgsum  24118  tsmssubm  24122  tsmsf1o  24124  utopsnneiplem  24226  ismet2  24312  prdsxmetlem  24347  elmopn2  24424  prdsbl  24470  metss  24487  metrest  24503  metcnp  24520  metcnp2  24521  metcn  24522  metucn  24550  nrginvrcn  24671  metdsge  24829  divcn  24849  elcncf2  24871  mulc1cncf  24886  cncfmet  24890  evth2  24941  lmmbr2  25240  lmmbrf  25243  iscfil2  25247  cfil3i  25250  iscau2  25258  iscau4  25260  iscauf  25261  caucfil  25264  iscmet3lem3  25271  cfilres  25277  causs  25279  lmclim  25284  rrxmet  25389  evthicc2  25441  cniccbdd  25442  ovolfioo  25448  ovolficc  25449  ismbl2  25508  mbfsup  25645  mbfinf  25646  mbflimsup  25647  0plef  25653  mbfi1flim  25704  xrge0f  25712  itg2mulclem  25727  itgeqa  25795  ellimc2  25858  ellimc3  25860  limcflf  25862  cnlimc  25869  dvferm1  25966  dvferm2  25968  rolle  25971  dvivthlem1  25989  ftc1lem6  26022  itgsubst  26030  mdegle0  26056  deg1leb  26074  plydivex  26278  ulm2  26367  ulmcaulem  26376  ulmcau  26377  ulmdvlem3  26384  abelthlem9  26422  abelth  26423  rlimcnp  26946  ftalem3  27056  issqf  27117  sqf11  27120  mpodvdsmulf1o  27175  dvdsmulf1o  27177  dchrelbas4  27224  dchrinv  27242  2sqlem6  27404  chpo1ubb  27462  dchrmusumlema  27474  dchrisum0lema  27495  ostth3  27619  ltsrec  27811  lrrecfr  27953  addsuniflem  28011  addbday  28028  negsunif  28065  n0fincut  28365  bdayfinbndlem1  28477  elreno2  28505  tgcgr4  28617  eqeelen  28991  brbtwn2  28992  colinearalg  28997  axcgrid  29003  axsegconlem1  29004  ax5seglem4  29019  ax5seglem5  29020  axbtwnid  29026  axpasch  29028  axeuclidlem  29049  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  axcontlem12  29062  elntg2  29072  isuvtx  29482  uvtx2vtx1edg  29485  uvtx2vtx1edgb  29486  iscplgrnb  29503  iscplgredg  29504  vdiscusgrb  29618  uhgrvd00  29622  upgriswlk  29728  wwlksnext  29980  clwwlkinwwlk  30129  clwwlkel  30135  clwwlkf  30136  clwwlkwwlksb  30143  wwlksext2clwwlk  30146  wwlksubclwwlk  30147  clwwlknonex2lem2  30197  nmounbi  30866  blocnilem  30894  isph  30912  phoeqi  30947  h2hcau  31069  h2hlm  31070  hial2eq2  31197  hoeq1  31920  hoeq2  31921  adjsym  31923  cnvadj  31982  hhcno  31994  hhcnf  31995  adjvalval  32027  leop2  32214  leoptri  32226  mdbr2  32386  dmdbr2  32393  mddmd2  32399  cdj3lem3b  32530  infxrge0gelb  32858  prodindf  32941  toslublem  33051  tosglblem  33053  mgccnv  33078  cntrval2  33251  submarchi  33266  isarchi3  33267  lindfpropd  33461  opprlidlabs  33564  ply1moneq  33667  psrmonmul  33713  cmpcref  34014  lmdvg  34117  eulerpartlemd  34530  subfacp1lem3  35384  subfacp1lem5  35386  satfv1lem  35564  dfrdg2  35995  opnrebl  36522  poimirlem23  37984  broucube  37995  itg2gt0cn  38016  ftc1cnnc  38033  lmclim2  38099  caures  38101  sstotbnd2  38115  rrnmet  38170  rrncmslem  38173  isdrngo3  38300  isidlc  38356  cvrval2  39740  isat3  39773  iscvlat2N  39790  glbconN  39843  ltrneq  40615  cdlemefrs29clN  40865  cdlemefrs32fva  40866  cdleme32fva  40903  cdlemk33N  41375  cdlemk34  41376  cdlemkid3N  41399  cdlemkid4  41400  diaglbN  41521  dibglbN  41632  dihglbcpreN  41766  dihglblem6  41806  hdmap1eulem  42288  hdmap1eulemOLDN  42289  hdmapoc  42397  hlhilocv  42423  primrootsunit1  42556  sn-sup3d  42957  fimgmcyc  42999  wepwsolem  43494  fnwe2lem2  43503  islnm2  43530  onmaxnelsup  43675  onsupnmax  43680  onsupuni  43681  onsupmaxb  43691  onsupeqnmax  43699  iscard5  43987  alephiso2  44009  clsk3nimkb  44491  ntrclsneine0  44516  ntrneineine0  44538  ntrneineine1  44539  ntrneicls00  44540  ntrneicls11  44541  ntrneiiso  44542  ntrneik2  44543  ntrneix2  44544  ntrneikb  44545  ntrneixb  44546  ntrneik3  44547  ntrneix3  44548  ntrneik13  44549  ntrneix13  44550  ntrneik4w  44551  ntrneik4  44552  caofcan  44774  modelac8prim  45443  infxrbnd2  45822  supminfxr  45916  rexanuz2nf  45944  evthiccabs  45950  ellimcabssub0  46071  climf  46076  clim2f  46088  clim2cf  46102  clim0cf  46106  limsupmnflem  46172  limsupre2lem  46176  limsupreuzmpt  46191  supcnvlimsup  46192  limsupge  46213  liminfreuzlem  46254  liminfltlem  46256  liminflimsupclim  46259  liminfpnfuz  46268  xlimpnfxnegmnf2  46310  fourierdlem70  46628  fourierdlem71  46629  fourierdlem73  46631  fourierdlem80  46638  fourierdlem83  46641  fourierdlem87  46645  voliunsge0lem  46924  meaiuninclem  46932  meaiuninc3v  46936  hoidmv1lelem3  47045  hoidmvlelem4  47050  hoidmvlelem5  47051  issmflem  47179  chnerlem1  47334  cfsetsnfsetf  47524  cfsetsnfsetfo  47526  nprmmul1  48005  requad2  48117  isubgrgrim  48423  grlicref  48506  islinindfis  48943  elbigolo1  49051  line2x  49248  itscnhlinecirc02p  49279  iscnrm3lem1  49427  ipolublem  49479  ipoglblem  49482  oppcup  49700  uptrlem3  49705  initopropd  49736  termopropd  49737  isinito2lem  49991  termc2  50011  lanup  50134  ranup  50135  aacllem  50294