Theorem ralbidva 3156

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

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

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 3051

This theorem is referenced by:  ralbidv  3158  2ralbidva  3197  raleqbidva  3301  poinxp  5704  soinxp  5705  frinxp  5706  ordunisssuc  6424  fnmptfvd  6986  funimass3  6999  fnnfpeq0  7124  cocan1  7237  cocan2  7238  isores2  7279  isoini2  7285  ofrfvalg  7630  ofrfval2  7643  caofidlcan  7660  tfindsg2  7804  f1oweALT  7916  fnsuppres  8133  dfsmo2  8279  smores  8284  smores2  8286  dfrecs3  8304  naddunif  8621  ac6sfi  9186  fimaxg  9189  ordunifi  9192  isfinite2  9200  fipreima  9260  supisolem  9379  fiming  9405  infempty  9414  ordiso2  9422  ordtypelem7  9431  cantnf  9604  wemapwe  9608  rankval3b  9740  rankonidlem  9742  iscard  9889  acndom  9963  dfac12lem3  10058  kmlem2  10064  cflim2  10175  cfsmolem  10182  ttukeylem6  10426  alephreg  10495  suplem2pr  10966  axsup  11210  sup3  12101  infm3  12103  suprleub  12110  dfinfre  12125  infregelb  12128  ofsubeq0  12144  ofsubge0  12146  zextlt  12568  prime  12575  suprfinzcl  12608  indstr  12831  supxr2  13231  supxrbnd1  13238  supxrbnd2  13239  supxrleub  13243  supxrbnd  13245  infxrgelb  13253  fzshftral  13533  mptnn0fsupp  13922  swrdspsleq  14591  pfxeq  14621  clim  15419  rlim  15420  clim2  15429  clim2c  15430  clim0c  15432  ello1mpt  15446  lo1o1  15457  o1lo1  15462  climabs0  15510  o1compt  15512  rlimdiv  15571  geomulcvg  15801  mertenslem2  15810  mertens  15811  rpnnen2lem12  16152  sqrt2irr  16176  fprodfvdvdsd  16263  fproddvdsd  16264  dfgcd2  16475  isprm7  16637  pc11  16810  pcz  16811  1arith  16857  vdwlem8  16918  vdwlem11  16921  vdw  16924  ramval  16938  pwsle  17415  mrieqvd  17563  mreacs  17583  cidpropd  17635  ismon2  17660  monpropd  17663  isepi  17666  isepi2  17667  subsubc  17779  funcres2b  17823  funcpropd  17828  isfull2  17839  isfth2  17843  fucsect  17901  fucinv  17902  pospropd  18250  ipodrsfi  18464  tsrss  18514  grpidpropd  18589  sgrppropd  18658  mndpropd  18686  smndex1mnd  18837  grppropd  18883  issubg4  19077  gass  19232  gsmsymgrfixlem1  19358  gsmsymgreqlem2  19362  gexdvds  19515  gexdvds2  19516  subgpgp  19528  sylow3lem6  19563  efgval2  19655  efgsp1  19668  dprdf11  19956  subgdmdprd  19967  rngpropd  20111  ringpropd  20225  abvpropd  20770  lsspropd  20971  lbspropd  21053  isridlrng  21176  isridl  21209  phlpropd  21612  ishil2  21676  frlmplusgvalb  21726  frlmvscavalb  21727  frlmvplusgscavalb  21728  lindfmm  21784  islindf4  21795  islindf5  21796  assapropd  21829  psrbaglefi  21884  psrbagconf1o  21887  gsumbagdiaglem  21888  mplmonmul  21993  gsumply1eq  22255  scmatf1  22477  cpmatmcllem  22664  cpmatmcl  22665  decpmataa0  22714  decpmatmulsumfsupp  22719  pmatcollpw2lem  22723  pm2mpmhmlem1  22764  tgss2  22933  isclo  23033  neips  23059  opnnei  23066  isperf3  23099  ssidcn  23201  lmbrf  23206  cnnei  23228  cnrest2  23232  lmss  23244  lmres  23246  ist1-2  23293  ist1-3  23295  isreg2  23323  cmpfi  23354  bwth  23356  1stccn  23409  subislly  23427  kgencn  23502  ptclsg  23561  ptcnplem  23567  xkococnlem  23605  xkoinjcn  23633  tgqtop  23658  qtopcn  23660  fbflim  23922  flimrest  23929  flfnei  23937  isflf  23939  cnflf  23948  fclsopn  23960  fclsbas  23967  fclsrest  23970  isfcf  23980  cnfcf  23988  ptcmplem3  24000  tmdgsum2  24042  eltsms  24079  tsmsgsum  24085  tsmssubm  24089  tsmsf1o  24091  utopsnneiplem  24193  ismet2  24279  prdsxmetlem  24314  elmopn2  24391  prdsbl  24437  metss  24454  metrest  24470  metcnp  24487  metcnp2  24488  metcn  24489  metucn  24517  nrginvrcn  24638  metdsge  24796  divcnOLD  24815  divcn  24817  elcncf2  24841  mulc1cncf  24856  cncfmet  24860  evth2  24917  lmmbr2  25217  lmmbrf  25220  iscfil2  25224  cfil3i  25227  iscau2  25235  iscau4  25237  iscauf  25238  caucfil  25241  iscmet3lem3  25248  cfilres  25254  causs  25256  lmclim  25261  rrxmet  25366  evthicc2  25419  cniccbdd  25420  ovolfioo  25426  ovolficc  25427  ismbl2  25486  mbfsup  25623  mbfinf  25624  mbflimsup  25625  0plef  25631  mbfi1flim  25682  xrge0f  25690  itg2mulclem  25705  itgeqa  25773  ellimc2  25836  ellimc3  25838  limcflf  25840  cnlimc  25847  dvferm1  25947  dvferm2  25949  rolle  25952  dvivthlem1  25971  ftc1lem6  26006  itgsubst  26014  mdegle0  26040  deg1leb  26058  plydivex  26263  ulm2  26352  ulmcaulem  26361  ulmcau  26362  ulmdvlem3  26369  abelthlem9  26408  abelth  26409  rlimcnp  26933  ftalem3  27043  issqf  27104  sqf11  27107  mpodvdsmulf1o  27162  dvdsmulf1o  27164  dchrelbas4  27212  dchrinv  27230  2sqlem6  27392  chpo1ubb  27450  dchrmusumlema  27462  dchrisum0lema  27483  ostth3  27607  sltrec  27797  lrrecfr  27923  addsuniflem  27981  addsbday  27998  negsunif  28035  n0sfincut  28333  bdayfinbndlem1  28444  elreno2  28472  tgcgr4  28584  eqeelen  28958  brbtwn2  28959  colinearalg  28964  axcgrid  28970  axsegconlem1  28971  ax5seglem4  28986  ax5seglem5  28987  axbtwnid  28993  axpasch  28995  axeuclidlem  29016  axcontlem2  29019  axcontlem4  29021  axcontlem7  29024  axcontlem12  29029  elntg2  29039  isuvtx  29449  uvtx2vtx1edg  29452  uvtx2vtx1edgb  29453  iscplgrnb  29470  iscplgredg  29471  vdiscusgrb  29585  uhgrvd00  29589  upgriswlk  29695  wwlksnext  29947  clwwlkinwwlk  30096  clwwlkel  30102  clwwlkf  30103  clwwlkwwlksb  30110  wwlksext2clwwlk  30113  wwlksubclwwlk  30114  clwwlknonex2lem2  30164  nmounbi  30832  blocnilem  30860  isph  30878  phoeqi  30913  h2hcau  31035  h2hlm  31036  hial2eq2  31163  hoeq1  31886  hoeq2  31887  adjsym  31889  cnvadj  31948  hhcno  31960  hhcnf  31961  adjvalval  31993  leop2  32180  leoptri  32192  mdbr2  32352  dmdbr2  32359  mddmd2  32365  cdj3lem3b  32496  infxrge0gelb  32825  prodindf  32923  toslublem  33033  tosglblem  33035  mgccnv  33060  cntrval2  33232  submarchi  33247  isarchi3  33248  lindfpropd  33442  opprlidlabs  33545  ply1moneq  33648  cmpcref  33986  lmdvg  34089  eulerpartlemd  34502  subfacp1lem3  35355  subfacp1lem5  35357  satfv1lem  35535  dfrdg2  35966  opnrebl  36493  poimirlem23  37813  broucube  37824  itg2gt0cn  37845  ftc1cnnc  37862  lmclim2  37928  caures  37930  sstotbnd2  37944  rrnmet  37999  rrncmslem  38002  isdrngo3  38129  isidlc  38185  cvrval2  39569  isat3  39602  iscvlat2N  39619  glbconN  39672  ltrneq  40444  cdlemefrs29clN  40694  cdlemefrs32fva  40695  cdleme32fva  40732  cdlemk33N  41204  cdlemk34  41205  cdlemkid3N  41228  cdlemkid4  41229  diaglbN  41350  dibglbN  41461  dihglbcpreN  41595  dihglblem6  41635  hdmap1eulem  42117  hdmap1eulemOLDN  42118  hdmapoc  42226  hlhilocv  42252  primrootsunit1  42386  sn-sup3d  42784  fimgmcyc  42826  wepwsolem  43321  fnwe2lem2  43330  islnm2  43357  onmaxnelsup  43502  onsupnmax  43507  onsupuni  43508  onsupmaxb  43518  onsupeqnmax  43526  iscard5  43814  alephiso2  43836  clsk3nimkb  44318  ntrclsneine0  44343  ntrneineine0  44365  ntrneineine1  44366  ntrneicls00  44367  ntrneicls11  44368  ntrneiiso  44369  ntrneik2  44370  ntrneix2  44371  ntrneikb  44372  ntrneixb  44373  ntrneik3  44374  ntrneix3  44375  ntrneik13  44376  ntrneix13  44377  ntrneik4w  44378  ntrneik4  44379  caofcan  44601  modelac8prim  45270  infxrbnd2  45650  supminfxr  45745  rexanuz2nf  45773  evthiccabs  45779  ellimcabssub0  45900  climf  45905  clim2f  45917  clim2cf  45931  clim0cf  45935  limsupmnflem  46001  limsupre2lem  46005  limsupreuzmpt  46020  supcnvlimsup  46021  limsupge  46042  liminfreuzlem  46083  liminfltlem  46085  liminflimsupclim  46088  liminfpnfuz  46097  xlimpnfxnegmnf2  46139  fourierdlem70  46457  fourierdlem71  46458  fourierdlem73  46460  fourierdlem80  46467  fourierdlem83  46470  fourierdlem87  46474  voliunsge0lem  46753  meaiuninclem  46761  meaiuninc3v  46765  hoidmv1lelem3  46874  hoidmvlelem4  46879  hoidmvlelem5  46880  issmflem  47008  chnerlem1  47163  cfsetsnfsetf  47341  cfsetsnfsetfo  47343  requad2  47906  isubgrgrim  48212  grlicref  48295  islinindfis  48732  elbigolo1  48840  line2x  49037  itscnhlinecirc02p  49068  iscnrm3lem1  49216  ipolublem  49268  ipoglblem  49271  oppcup  49489  uptrlem3  49494  initopropd  49525  termopropd  49526  isinito2lem  49780  termc2  49800  lanup  49923  ranup  49924  aacllem  50083