Theorem ralbidva 3162

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ral 3056

This theorem is referenced by:  ralbidv  3164  2ralbidva  3203  raleqbidva  3305  poinxp  5702  soinxp  5703  frinxp  5704  ordunisssuc  6422  fnmptfvd  6986  funimass3  6999  fnnfpeq0  7126  cocan1  7239  cocan2  7240  isores2  7281  isoini2  7287  ofrfvalg  7632  ofrfval2  7645  caofidlcan  7662  tfindsg2  7806  f1oweALT  7918  fnsuppres  8135  dfsmo2  8281  smores  8286  smores2  8288  dfrecs3  8306  naddunif  8623  ac6sfi  9188  fimaxg  9191  ordunifi  9194  isfinite2  9202  fipreima  9262  supisolem  9381  fiming  9407  infempty  9416  ordiso2  9424  ordtypelem7  9433  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  20811  lsspropd  21011  lbspropd  21093  isridlrng  21216  isridl  21249  phlpropd  21634  ishil2  21698  frlmplusgvalb  21748  frlmvscavalb  21749  frlmvplusgscavalb  21750  lindfmm  21806  islindf4  21817  islindf5  21818  assapropd  21850  psrbaglefi  21905  psrbagconf1o  21908  gsumbagdiaglem  21910  mplmonmul  22016  gsumply1eq  22299  scmatf1  22518  cpmatmcllem  22705  cpmatmcl  22706  decpmataa0  22755  decpmatmulsumfsupp  22760  pmatcollpw2lem  22764  pm2mpmhmlem1  22805  tgss2  22974  isclo  23074  neips  23100  opnnei  23107  isperf3  23140  ssidcn  23242  lmbrf  23247  cnnei  23269  cnrest2  23273  lmss  23285  lmres  23287  ist1-2  23334  ist1-3  23336  isreg2  23364  cmpfi  23395  bwth  23397  1stccn  23450  subislly  23468  kgencn  23543  ptclsg  23602  ptcnplem  23608  xkococnlem  23646  xkoinjcn  23674  tgqtop  23699  qtopcn  23701  fbflim  23963  flimrest  23970  flfnei  23978  isflf  23980  cnflf  23989  fclsopn  24001  fclsbas  24008  fclsrest  24011  isfcf  24021  cnfcf  24029  ptcmplem3  24041  tmdgsum2  24083  eltsms  24120  tsmsgsum  24126  tsmssubm  24130  tsmsf1o  24132  utopsnneiplem  24234  ismet2  24320  prdsxmetlem  24355  elmopn2  24432  prdsbl  24478  metss  24495  metrest  24511  metcnp  24528  metcnp2  24529  metcn  24530  metucn  24558  nrginvrcn  24679  metdsge  24837  divcn  24857  elcncf2  24879  mulc1cncf  24894  cncfmet  24898  evth2  24949  lmmbr2  25248  lmmbrf  25251  iscfil2  25255  cfil3i  25258  iscau2  25266  iscau4  25268  iscauf  25269  caucfil  25272  iscmet3lem3  25279  cfilres  25285  causs  25287  lmclim  25292  rrxmet  25397  evthicc2  25449  cniccbdd  25450  ovolfioo  25456  ovolficc  25457  ismbl2  25516  mbfsup  25653  mbfinf  25654  mbflimsup  25655  0plef  25661  mbfi1flim  25712  xrge0f  25720  itg2mulclem  25735  itgeqa  25803  ellimc2  25866  ellimc3  25868  limcflf  25870  cnlimc  25877  dvferm1  25974  dvferm2  25976  rolle  25979  dvivthlem1  25997  ftc1lem6  26030  itgsubst  26038  mdegle0  26064  deg1leb  26082  plydivex  26285  ulm2  26372  ulmcaulem  26381  ulmcau  26382  ulmdvlem3  26389  abelthlem9  26427  abelth  26428  rlimcnp  26951  ftalem3  27060  issqf  27121  sqf11  27124  mpodvdsmulf1o  27179  dvdsmulf1o  27181  dchrelbas4  27228  dchrinv  27246  2sqlem6  27408  chpo1ubb  27466  dchrmusumlema  27478  dchrisum0lema  27499  ostth3  27623  ltsrec  27815  lrrecfr  27957  addsuniflem  28015  addbday  28032  negsunif  28069  n0fincut  28369  bdayfinbndlem1  28481  elreno2  28509  tgcgr4  28621  eqeelen  28995  brbtwn2  28996  colinearalg  29001  axcgrid  29007  axsegconlem1  29008  ax5seglem4  29023  ax5seglem5  29024  axbtwnid  29030  axpasch  29032  axeuclidlem  29053  axcontlem2  29056  axcontlem4  29058  axcontlem7  29061  axcontlem12  29066  elntg2  29076  isuvtx  29486  uvtx2vtx1edg  29489  uvtx2vtx1edgb  29490  iscplgrnb  29507  iscplgredg  29508  vdiscusgrb  29621  uhgrvd00  29625  upgriswlk  29731  wwlksnext  29983  clwwlkinwwlk  30132  clwwlkel  30138  clwwlkf  30139  clwwlkwwlksb  30146  wwlksext2clwwlk  30149  wwlksubclwwlk  30150  clwwlknonex2lem2  30200  nmounbi  30869  blocnilem  30897  isph  30915  phoeqi  30950  h2hcau  31072  h2hlm  31073  hial2eq2  31200  hoeq1  31923  hoeq2  31924  adjsym  31926  cnvadj  31985  hhcno  31997  hhcnf  31998  adjvalval  32030  leop2  32217  leoptri  32229  mdbr2  32389  dmdbr2  32396  mddmd2  32402  cdj3lem3b  32533  infxrge0gelb  32862  prodindf  32945  toslublem  33055  tosglblem  33057  mgccnv  33082  cntrval2  33256  submarchi  33271  isarchi3  33272  lindfpropd  33469  opprlidlabs  33572  ply1moneq  33683  psrmonmul  33746  cmpcref  34046  lmdvg  34149  eulerpartlemd  34562  subfacp1lem3  35425  subfacp1lem5  35427  satfv1lem  35605  dfrdg2  36036  opnrebl  36563  poimirlem23  38025  broucube  38036  itg2gt0cn  38057  ftc1cnnc  38074  lmclim2  38140  caures  38142  sstotbnd2  38156  rrnmet  38211  rrncmslem  38214  isdrngo3  38341  isidlc  38397  cvrval2  39781  isat3  39814  iscvlat2N  39831  glbconN  39884  ltrneq  40656  cdlemefrs29clN  40906  cdlemefrs32fva  40907  cdleme32fva  40944  cdlemk33N  41416  cdlemk34  41417  cdlemkid3N  41440  cdlemkid4  41441  diaglbN  41562  dibglbN  41673  dihglbcpreN  41807  dihglblem6  41847  hdmap1eulem  42329  hdmap1eulemOLDN  42330  hdmapoc  42438  hlhilocv  42464  primrootsunit1  42597  sn-sup3d  42997  fimgmcyc  43035  wepwsolem  43502  fnwe2lem2  43511  islnm2  43538  onmaxnelsup  43683  onsupnmax  43688  onsupuni  43689  onsupmaxb  43699  onsupeqnmax  43707  iscard5  43995  alephiso2  44017  clsk3nimkb  44499  ntrclsneine0  44524  ntrneineine0  44546  ntrneineine1  44547  ntrneicls00  44548  ntrneicls11  44549  ntrneiiso  44550  ntrneik2  44551  ntrneix2  44552  ntrneikb  44553  ntrneixb  44554  ntrneik3  44555  ntrneix3  44556  ntrneik13  44557  ntrneix13  44558  ntrneik4w  44559  ntrneik4  44560  caofcan  44782  modelac8prim  45451  infxrbnd2  45827  supminfxr  45921  rexanuz2nf  45949  evthiccabs  45955  ellimcabssub0  46076  climf  46081  clim2f  46093  clim2cf  46107  clim0cf  46111  limsupmnflem  46177  limsupre2lem  46181  limsupreuzmpt  46196  supcnvlimsup  46197  limsupge  46218  liminfreuzlem  46259  liminfltlem  46261  liminflimsupclim  46264  liminfpnfuz  46273  xlimpnfxnegmnf2  46315  fourierdlem70  46633  fourierdlem71  46634  fourierdlem73  46636  fourierdlem80  46643  fourierdlem83  46646  fourierdlem87  46650  voliunsge0lem  46929  meaiuninclem  46937  meaiuninc3v  46941  hoidmv1lelem3  47050  hoidmvlelem4  47055  hoidmvlelem5  47056  issmflem  47184  chnerlem1  47341  cfsetsnfsetf  47535  cfsetsnfsetfo  47537  nprmmul1  48016  requad2  48128  isubgrgrim  48434  grlicref  48517  islinindfis  48954  elbigolo1  49062  line2x  49259  itscnhlinecirc02p  49290  iscnrm3lem1  49438  ipolublem  49490  ipoglblem  49493  oppcup  49711  uptrlem3  49716  initopropd  49747  termopropd  49748  isinito2lem  50002  termc2  50022  lanup  50145  ranup  50146  aacllem  50305