Theorem ralbidva 3173

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3059

This theorem is referenced by:  ralbidv  3175  2ralbidva  3216  raleqbidva  3329  poinxp  5768  soinxp  5769  frinxp  5770  ordunisssuc  6491  fnmptfvd  7060  funimass3  7073  fnnfpeq0  7197  cocan1  7310  cocan2  7311  isores2  7352  isoini2  7358  ofrfvalg  7704  ofrfval2  7717  tfindsg2  7882  f1oweALT  7995  fnsuppres  8214  dfsmo2  8385  smores  8390  smores2  8392  dfrecs3  8410  dfrecs3OLD  8411  naddunif  8729  ac6sfi  9317  fimaxg  9320  ordunifi  9323  isfinite2  9331  fipreima  9395  supisolem  9510  fiming  9535  infempty  9544  ordiso2  9552  ordtypelem7  9561  cantnf  9730  wemapwe  9734  rankval3b  9863  rankonidlem  9865  iscard  10012  acndom  10088  dfac12lem3  10183  kmlem2  10189  cflim2  10300  cfsmolem  10307  ttukeylem6  10551  alephreg  10619  suplem2pr  11090  axsup  11333  sup3  12222  infm3  12224  suprleub  12231  dfinfre  12246  infregelb  12249  ofsubeq0  12260  ofsubge0  12262  zextlt  12689  prime  12696  suprfinzcl  12729  indstr  12955  supxr2  13352  supxrbnd1  13359  supxrbnd2  13360  supxrleub  13364  supxrbnd  13366  infxrgelb  13373  fzshftral  13651  mptnn0fsupp  14034  swrdspsleq  14699  pfxeq  14730  clim  15526  rlim  15527  clim2  15536  clim2c  15537  clim0c  15539  ello1mpt  15553  lo1o1  15564  o1lo1  15569  climabs0  15617  o1compt  15619  rlimdiv  15678  geomulcvg  15908  mertenslem2  15917  mertens  15918  rpnnen2lem12  16257  sqrt2irr  16281  fprodfvdvdsd  16367  fproddvdsd  16368  dfgcd2  16579  isprm7  16741  pc11  16913  pcz  16914  1arith  16960  vdwlem8  17021  vdwlem11  17024  vdw  17027  ramval  17041  pwsle  17538  mrieqvd  17682  mreacs  17702  cidpropd  17754  ismon2  17781  monpropd  17784  isepi  17787  isepi2  17788  subsubc  17903  funcres2b  17947  funcpropd  17953  isfull2  17964  isfth2  17968  fucsect  18028  fucinv  18029  pospropd  18384  ipodrsfi  18596  tsrss  18646  grpidpropd  18687  sgrppropd  18756  mndpropd  18784  smndex1mnd  18935  grppropd  18981  issubg4  19175  gass  19331  gsmsymgrfixlem1  19459  gsmsymgreqlem2  19463  gexdvds  19616  gexdvds2  19617  subgpgp  19629  sylow3lem6  19664  efgval2  19756  efgsp1  19769  dprdf11  20057  subgdmdprd  20068  rngpropd  20191  ringpropd  20301  abvpropd  20852  lsspropd  21033  lbspropd  21115  isridlrng  21246  isridl  21279  phlpropd  21690  ishil2  21756  frlmplusgvalb  21806  frlmvscavalb  21807  frlmvplusgscavalb  21808  lindfmm  21864  islindf4  21875  islindf5  21876  assapropd  21909  psrbaglefi  21963  psrbagconf1o  21966  gsumbagdiaglem  21967  mplmonmul  22071  gsumply1eq  22328  scmatf1  22552  cpmatmcllem  22739  cpmatmcl  22740  decpmataa0  22789  decpmatmulsumfsupp  22794  pmatcollpw2lem  22798  pm2mpmhmlem1  22839  tgss2  23009  isclo  23110  neips  23136  opnnei  23143  isperf3  23176  ssidcn  23278  lmbrf  23283  cnnei  23305  cnrest2  23309  lmss  23321  lmres  23323  ist1-2  23370  ist1-3  23372  isreg2  23400  cmpfi  23431  bwth  23433  1stccn  23486  subislly  23504  kgencn  23579  ptclsg  23638  ptcnplem  23644  xkococnlem  23682  xkoinjcn  23710  tgqtop  23735  qtopcn  23737  fbflim  23999  flimrest  24006  flfnei  24014  isflf  24016  cnflf  24025  fclsopn  24037  fclsbas  24044  fclsrest  24047  isfcf  24057  cnfcf  24065  ptcmplem3  24077  tmdgsum2  24119  eltsms  24156  tsmsgsum  24162  tsmssubm  24166  tsmsf1o  24168  utopsnneiplem  24271  ismet2  24358  prdsxmetlem  24393  elmopn2  24470  prdsbl  24519  metss  24536  metrest  24552  metcnp  24569  metcnp2  24570  metcn  24571  metucn  24599  nrginvrcn  24728  metdsge  24884  divcnOLD  24903  divcn  24905  elcncf2  24929  mulc1cncf  24944  cncfmet  24948  evth2  25005  lmmbr2  25306  lmmbrf  25309  iscfil2  25313  cfil3i  25316  iscau2  25324  iscau4  25326  iscauf  25327  caucfil  25330  iscmet3lem3  25337  cfilres  25343  causs  25345  lmclim  25350  rrxmet  25455  evthicc2  25508  cniccbdd  25509  ovolfioo  25515  ovolficc  25516  ismbl2  25575  mbfsup  25712  mbfinf  25713  mbflimsup  25714  0plef  25720  mbfi1flim  25772  xrge0f  25780  itg2mulclem  25795  itgeqa  25863  ellimc2  25926  ellimc3  25928  limcflf  25930  cnlimc  25937  dvferm1  26037  dvferm2  26039  rolle  26042  dvivthlem1  26061  ftc1lem6  26096  itgsubst  26104  mdegle0  26130  deg1leb  26148  plydivex  26353  ulm2  26442  ulmcaulem  26451  ulmcau  26452  ulmdvlem3  26459  abelthlem9  26498  abelth  26499  rlimcnp  27022  ftalem3  27132  issqf  27193  sqf11  27196  mpodvdsmulf1o  27251  dvdsmulf1o  27253  dchrelbas4  27301  dchrinv  27319  2sqlem6  27481  chpo1ubb  27539  dchrmusumlema  27551  dchrisum0lema  27572  ostth3  27696  sltrec  27879  lrrecfr  27990  addsuniflem  28048  addsbday  28064  negsunif  28101  tgcgr4  28553  eqeelen  28933  brbtwn2  28934  colinearalg  28939  axcgrid  28945  axsegconlem1  28946  ax5seglem4  28961  ax5seglem5  28962  axbtwnid  28968  axpasch  28970  axeuclidlem  28991  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem12  29004  elntg2  29014  isuvtx  29426  uvtx2vtx1edg  29429  uvtx2vtx1edgb  29430  iscplgrnb  29447  iscplgredg  29448  vdiscusgrb  29562  uhgrvd00  29566  upgriswlk  29673  wwlksnext  29922  clwwlkinwwlk  30068  clwwlkel  30074  clwwlkf  30075  clwwlkwwlksb  30082  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  clwwlknonex2lem2  30136  nmounbi  30804  blocnilem  30832  isph  30850  phoeqi  30885  h2hcau  31007  h2hlm  31008  hial2eq2  31135  hoeq1  31858  hoeq2  31859  adjsym  31861  cnvadj  31920  hhcno  31932  hhcnf  31933  adjvalval  31965  leop2  32152  leoptri  32164  mdbr2  32324  dmdbr2  32331  mddmd2  32337  cdj3lem3b  32468  infxrge0gelb  32776  toslublem  32946  tosglblem  32948  mgccnv  32973  submarchi  33175  isarchi3  33176  lindfpropd  33389  opprlidlabs  33492  ply1moneq  33590  cmpcref  33810  lmdvg  33913  prodindf  34003  eulerpartlemd  34347  subfacp1lem3  35166  subfacp1lem5  35168  satfv1lem  35346  dfrdg2  35776  opnrebl  36302  poimirlem23  37629  broucube  37640  itg2gt0cn  37661  ftc1cnnc  37678  lmclim2  37744  caures  37746  sstotbnd2  37760  rrnmet  37815  rrncmslem  37818  isdrngo3  37945  isidlc  38001  cvrval2  39255  isat3  39288  iscvlat2N  39305  glbconN  39358  glbconNOLD  39359  ltrneq  40131  cdlemefrs29clN  40381  cdlemefrs32fva  40382  cdleme32fva  40419  cdlemk33N  40891  cdlemk34  40892  cdlemkid3N  40915  cdlemkid4  40916  diaglbN  41037  dibglbN  41148  dihglbcpreN  41282  dihglblem6  41322  hdmap1eulem  41804  hdmap1eulemOLDN  41805  hdmapoc  41913  hlhilocv  41943  primrootsunit1  42078  sn-sup3d  42478  fimgmcyc  42520  wepwsolem  43030  fnwe2lem2  43039  islnm2  43066  onmaxnelsup  43211  onsupnmax  43216  onsupuni  43217  onsupmaxb  43227  onsupeqnmax  43235  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  44318  infxrbnd2  45318  supminfxr  45413  rexanuz2nf  45442  evthiccabs  45448  ellimcabssub0  45572  climf  45577  clim2f  45591  clim2cf  45605  clim0cf  45609  limsupmnflem  45675  limsupre2lem  45679  limsupreuzmpt  45694  supcnvlimsup  45695  limsupge  45716  liminfreuzlem  45757  liminfltlem  45759  liminflimsupclim  45762  liminfpnfuz  45771  xlimpnfxnegmnf2  45813  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem80  46141  fourierdlem83  46144  fourierdlem87  46148  voliunsge0lem  46427  meaiuninclem  46435  meaiuninc3v  46439  hoidmv1lelem3  46548  hoidmvlelem4  46553  hoidmvlelem5  46554  issmflem  46682  cfsetsnfsetf  47007  cfsetsnfsetfo  47009  requad2  47547  isubgrgrim  47834  grlicref  47907  islinindfis  48294  elbigolo1  48406  line2x  48603  itscnhlinecirc02p  48634  iscnrm3lem1  48729  ipolublem  48774  ipoglblem  48777  aacllem  49031