Theorem ralbidva 3119

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  ralbidv  3120  2ralbidva  3121  raleqbidva  3345  poinxp  5658  soinxp  5659  frinxp  5660  ordunisssuc  6353  fnmptfvd  6900  funimass3  6913  fnnfpeq0  7032  cocan1  7143  cocan2  7144  isores2  7184  isoini2  7190  ofrfvalg  7519  ofrfval2  7532  tfindsg2  7683  f1oweALT  7788  fnsuppres  7978  dfsmo2  8149  smores  8154  smores2  8156  dfrecs3  8174  dfrecs3OLD  8175  ac6sfi  8988  fimaxg  8991  ordunifi  8994  isfinite2  9002  fipreima  9055  supisolem  9162  fiming  9187  infempty  9196  ordiso2  9204  ordtypelem7  9213  cantnf  9381  wemapwe  9385  rankval3b  9515  rankonidlem  9517  iscard  9664  acndom  9738  dfac12lem3  9832  kmlem2  9838  cflim2  9950  cfsmolem  9957  ttukeylem6  10201  alephreg  10269  suplem2pr  10740  axsup  10981  sup3  11862  infm3  11864  suprleub  11871  dfinfre  11886  infregelb  11889  ofsubeq0  11900  ofsubge0  11902  zextlt  12324  prime  12331  suprfinzcl  12365  indstr  12585  supxr2  12977  supxrbnd1  12984  supxrbnd2  12985  supxrleub  12989  supxrbnd  12991  infxrgelb  12998  fzshftral  13273  mptnn0fsupp  13645  swrdspsleq  14306  pfxeq  14337  clim  15131  rlim  15132  clim2  15141  clim2c  15142  clim0c  15144  ello1mpt  15158  lo1o1  15169  o1lo1  15174  climabs0  15222  o1compt  15224  rlimdiv  15285  geomulcvg  15516  mertenslem2  15525  mertens  15526  rpnnen2lem12  15862  sqrt2irr  15886  fprodfvdvdsd  15971  fproddvdsd  15972  dfgcd2  16182  isprm7  16341  pc11  16509  pcz  16510  1arith  16556  vdwlem8  16617  vdwlem11  16620  vdw  16623  ramval  16637  pwsle  17120  mrieqvd  17264  mreacs  17284  cidpropd  17336  ismon2  17363  monpropd  17366  isepi  17369  isepi2  17370  subsubc  17484  funcres2b  17528  funcpropd  17532  isfull2  17543  isfth2  17547  fucsect  17606  fucinv  17607  pospropd  17960  ipodrsfi  18172  tsrss  18222  grpidpropd  18261  mndpropd  18325  smndex1mnd  18464  grppropd  18509  issubg4  18689  gass  18822  gsmsymgrfixlem1  18950  gsmsymgreqlem2  18954  gexdvds  19104  gexdvds2  19105  subgpgp  19117  sylow3lem6  19152  efgval2  19245  efgsp1  19258  dprdf11  19541  subgdmdprd  19552  ringpropd  19736  abvpropd  20017  lsspropd  20194  lbspropd  20276  phlpropd  20772  ishil2  20836  frlmplusgvalb  20886  frlmvscavalb  20887  frlmvplusgscavalb  20888  lindfmm  20944  islindf4  20955  islindf5  20956  assapropd  20986  psrbaglefi  21045  psrbaglefiOLD  21046  psrbagconf1o  21049  psrbagconf1oOLD  21050  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  mplmonmul  21147  gsumply1eq  21386  scmatf1  21588  cpmatmcllem  21775  cpmatmcl  21776  decpmataa0  21825  decpmatmulsumfsupp  21830  pmatcollpw2lem  21834  pm2mpmhmlem1  21875  tgss2  22045  isclo  22146  neips  22172  opnnei  22179  isperf3  22212  ssidcn  22314  lmbrf  22319  cnnei  22341  cnrest2  22345  lmss  22357  lmres  22359  ist1-2  22406  ist1-3  22408  isreg2  22436  cmpfi  22467  bwth  22469  1stccn  22522  subislly  22540  kgencn  22615  ptclsg  22674  ptcnplem  22680  xkococnlem  22718  xkoinjcn  22746  tgqtop  22771  qtopcn  22773  fbflim  23035  flimrest  23042  flfnei  23050  isflf  23052  cnflf  23061  fclsopn  23073  fclsbas  23080  fclsrest  23083  isfcf  23093  cnfcf  23101  ptcmplem3  23113  tmdgsum2  23155  eltsms  23192  tsmsgsum  23198  tsmssubm  23202  tsmsf1o  23204  utopsnneiplem  23307  ismet2  23394  prdsxmetlem  23429  elmopn2  23506  prdsbl  23553  metss  23570  metrest  23586  metcnp  23603  metcnp2  23604  metcn  23605  metucn  23633  nrginvrcn  23762  metdsge  23918  divcn  23937  elcncf2  23959  mulc1cncf  23974  cncfmet  23978  evth2  24029  lmmbr2  24328  lmmbrf  24331  iscfil2  24335  cfil3i  24338  iscau2  24346  iscau4  24348  iscauf  24349  caucfil  24352  iscmet3lem3  24359  cfilres  24365  causs  24367  lmclim  24372  rrxmet  24477  evthicc2  24529  cniccbdd  24530  ovolfioo  24536  ovolficc  24537  ismbl2  24596  mbfsup  24733  mbfinf  24734  mbflimsup  24735  0plef  24741  mbfi1flim  24793  xrge0f  24801  itg2mulclem  24816  itgeqa  24883  ellimc2  24946  ellimc3  24948  limcflf  24950  cnlimc  24957  dvferm1  25054  dvferm2  25056  rolle  25059  dvivthlem1  25077  ftc1lem6  25110  itgsubst  25118  mdegle0  25147  deg1leb  25165  plydivex  25362  ulm2  25449  ulmcaulem  25458  ulmcau  25459  ulmdvlem3  25466  abelthlem9  25504  abelth  25505  rlimcnp  26020  ftalem3  26129  issqf  26190  sqf11  26193  dvdsmulf1o  26248  dchrelbas4  26296  dchrinv  26314  2sqlem6  26476  chpo1ubb  26534  dchrmusumlema  26546  dchrisum0lema  26567  ostth3  26691  tgcgr4  26796  eqeelen  27175  brbtwn2  27176  colinearalg  27181  axcgrid  27187  axsegconlem1  27188  ax5seglem4  27203  ax5seglem5  27204  axbtwnid  27210  axpasch  27212  axeuclidlem  27233  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem12  27246  elntg2  27256  isuvtx  27665  uvtx2vtx1edg  27668  uvtx2vtx1edgb  27669  iscplgrnb  27686  iscplgredg  27687  vdiscusgrb  27800  uhgrvd00  27804  upgriswlk  27910  wwlksnext  28159  clwwlkinwwlk  28305  clwwlkel  28311  clwwlkf  28312  clwwlkwwlksb  28319  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  clwwlknonex2lem2  28373  nmounbi  29039  blocnilem  29067  isph  29085  phoeqi  29120  h2hcau  29242  h2hlm  29243  hial2eq2  29370  hoeq1  30093  hoeq2  30094  adjsym  30096  cnvadj  30155  hhcno  30167  hhcnf  30168  adjvalval  30200  leop2  30387  leoptri  30399  mdbr2  30559  dmdbr2  30566  mddmd2  30572  cdj3lem3b  30703  infxrge0gelb  30991  toslublem  31152  tosglblem  31154  mgccnv  31179  submarchi  31342  isarchi3  31343  lindfpropd  31478  cmpcref  31702  lmdvg  31805  prodindf  31891  eulerpartlemd  32233  subfacp1lem3  33044  subfacp1lem5  33046  satfv1lem  33224  dfrdg2  33677  sltrec  33941  lrrecfr  34027  opnrebl  34436  poimirlem23  35727  broucube  35738  itg2gt0cn  35759  ftc1cnnc  35776  lmclim2  35843  caures  35845  sstotbnd2  35859  rrnmet  35914  rrncmslem  35917  isdrngo3  36044  isidlc  36100  cvrval2  37215  isat3  37248  iscvlat2N  37265  glbconN  37318  ltrneq  38090  cdlemefrs29clN  38340  cdlemefrs32fva  38341  cdleme32fva  38378  cdlemk33N  38850  cdlemk34  38851  cdlemkid3N  38874  cdlemkid4  38875  diaglbN  38996  dibglbN  39107  dihglbcpreN  39241  dihglblem6  39281  hdmap1eulem  39763  hdmap1eulemOLDN  39764  hdmapoc  39872  hlhilocv  39902  wepwsolem  40783  fnwe2lem2  40792  islnm2  40819  iscard5  41039  alephiso2  41054  clsk3nimkb  41539  ntrclsneine0  41564  ntrneineine0  41586  ntrneineine1  41587  ntrneicls00  41588  ntrneicls11  41589  ntrneiiso  41590  ntrneik2  41591  ntrneix2  41592  ntrneikb  41593  ntrneixb  41594  ntrneik3  41595  ntrneix3  41596  ntrneik13  41597  ntrneix13  41598  ntrneik4w  41599  ntrneik4  41600  caofcan  41830  infxrbnd2  42798  supminfxr  42894  evthiccabs  42924  ellimcabssub0  43048  climf  43053  clim2f  43067  clim2cf  43081  clim0cf  43085  limsupmnflem  43151  limsupre2lem  43155  limsupreuzmpt  43170  supcnvlimsup  43171  limsupge  43192  liminfreuzlem  43233  liminfltlem  43235  liminflimsupclim  43238  liminfpnfuz  43247  xlimpnfxnegmnf2  43289  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem80  43617  fourierdlem83  43620  fourierdlem87  43624  voliunsge0lem  43900  meaiuninclem  43908  meaiuninc3v  43912  hoidmv1lelem3  44021  hoidmvlelem4  44026  hoidmvlelem5  44027  issmflem  44150  cfsetsnfsetf  44439  cfsetsnfsetfo  44441  requad2  44963  islinindfis  45678  elbigolo1  45791  line2x  45988  itscnhlinecirc02p  46019  iscnrm3lem1  46115  ipolublem  46160  ipoglblem  46163  aacllem  46391