Theorem ralbidva 3155

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralbidv  3157  2ralbidva  3200  raleqbidva  3307  poinxp  5722  soinxp  5723  frinxp  5724  ordunisssuc  6443  fnmptfvd  7016  funimass3  7029  fnnfpeq0  7155  cocan1  7269  cocan2  7270  isores2  7311  isoini2  7317  ofrfvalg  7664  ofrfval2  7677  caofidlcan  7694  tfindsg2  7841  f1oweALT  7954  fnsuppres  8173  dfsmo2  8319  smores  8324  smores2  8326  dfrecs3  8344  naddunif  8660  ac6sfi  9238  fimaxg  9241  ordunifi  9244  isfinite2  9252  fipreima  9316  supisolem  9432  fiming  9458  infempty  9467  ordiso2  9475  ordtypelem7  9484  cantnf  9653  wemapwe  9657  rankval3b  9786  rankonidlem  9788  iscard  9935  acndom  10011  dfac12lem3  10106  kmlem2  10112  cflim2  10223  cfsmolem  10230  ttukeylem6  10474  alephreg  10542  suplem2pr  11013  axsup  11256  sup3  12147  infm3  12149  suprleub  12156  dfinfre  12171  infregelb  12174  ofsubeq0  12190  ofsubge0  12192  zextlt  12615  prime  12622  suprfinzcl  12655  indstr  12882  supxr2  13281  supxrbnd1  13288  supxrbnd2  13289  supxrleub  13293  supxrbnd  13295  infxrgelb  13303  fzshftral  13583  mptnn0fsupp  13969  swrdspsleq  14637  pfxeq  14668  clim  15467  rlim  15468  clim2  15477  clim2c  15478  clim0c  15480  ello1mpt  15494  lo1o1  15505  o1lo1  15510  climabs0  15558  o1compt  15560  rlimdiv  15619  geomulcvg  15849  mertenslem2  15858  mertens  15859  rpnnen2lem12  16200  sqrt2irr  16224  fprodfvdvdsd  16311  fproddvdsd  16312  dfgcd2  16523  isprm7  16685  pc11  16858  pcz  16859  1arith  16905  vdwlem8  16966  vdwlem11  16969  vdw  16972  ramval  16986  pwsle  17462  mrieqvd  17606  mreacs  17626  cidpropd  17678  ismon2  17703  monpropd  17706  isepi  17709  isepi2  17710  subsubc  17822  funcres2b  17866  funcpropd  17871  isfull2  17882  isfth2  17886  fucsect  17944  fucinv  17945  pospropd  18293  ipodrsfi  18505  tsrss  18555  grpidpropd  18596  sgrppropd  18665  mndpropd  18693  smndex1mnd  18844  grppropd  18890  issubg4  19084  gass  19240  gsmsymgrfixlem1  19364  gsmsymgreqlem2  19368  gexdvds  19521  gexdvds2  19522  subgpgp  19534  sylow3lem6  19569  efgval2  19661  efgsp1  19674  dprdf11  19962  subgdmdprd  19973  rngpropd  20090  ringpropd  20204  abvpropd  20751  lsspropd  20931  lbspropd  21013  isridlrng  21136  isridl  21169  phlpropd  21571  ishil2  21635  frlmplusgvalb  21685  frlmvscavalb  21686  frlmvplusgscavalb  21687  lindfmm  21743  islindf4  21754  islindf5  21755  assapropd  21788  psrbaglefi  21842  psrbagconf1o  21845  gsumbagdiaglem  21846  mplmonmul  21950  gsumply1eq  22203  scmatf1  22425  cpmatmcllem  22612  cpmatmcl  22613  decpmataa0  22662  decpmatmulsumfsupp  22667  pmatcollpw2lem  22671  pm2mpmhmlem1  22712  tgss2  22881  isclo  22981  neips  23007  opnnei  23014  isperf3  23047  ssidcn  23149  lmbrf  23154  cnnei  23176  cnrest2  23180  lmss  23192  lmres  23194  ist1-2  23241  ist1-3  23243  isreg2  23271  cmpfi  23302  bwth  23304  1stccn  23357  subislly  23375  kgencn  23450  ptclsg  23509  ptcnplem  23515  xkococnlem  23553  xkoinjcn  23581  tgqtop  23606  qtopcn  23608  fbflim  23870  flimrest  23877  flfnei  23885  isflf  23887  cnflf  23896  fclsopn  23908  fclsbas  23915  fclsrest  23918  isfcf  23928  cnfcf  23936  ptcmplem3  23948  tmdgsum2  23990  eltsms  24027  tsmsgsum  24033  tsmssubm  24037  tsmsf1o  24039  utopsnneiplem  24142  ismet2  24228  prdsxmetlem  24263  elmopn2  24340  prdsbl  24386  metss  24403  metrest  24419  metcnp  24436  metcnp2  24437  metcn  24438  metucn  24466  nrginvrcn  24587  metdsge  24745  divcnOLD  24764  divcn  24766  elcncf2  24790  mulc1cncf  24805  cncfmet  24809  evth2  24866  lmmbr2  25166  lmmbrf  25169  iscfil2  25173  cfil3i  25176  iscau2  25184  iscau4  25186  iscauf  25187  caucfil  25190  iscmet3lem3  25197  cfilres  25203  causs  25205  lmclim  25210  rrxmet  25315  evthicc2  25368  cniccbdd  25369  ovolfioo  25375  ovolficc  25376  ismbl2  25435  mbfsup  25572  mbfinf  25573  mbflimsup  25574  0plef  25580  mbfi1flim  25631  xrge0f  25639  itg2mulclem  25654  itgeqa  25722  ellimc2  25785  ellimc3  25787  limcflf  25789  cnlimc  25796  dvferm1  25896  dvferm2  25898  rolle  25901  dvivthlem1  25920  ftc1lem6  25955  itgsubst  25963  mdegle0  25989  deg1leb  26007  plydivex  26212  ulm2  26301  ulmcaulem  26310  ulmcau  26311  ulmdvlem3  26318  abelthlem9  26357  abelth  26358  rlimcnp  26882  ftalem3  26992  issqf  27053  sqf11  27056  mpodvdsmulf1o  27111  dvdsmulf1o  27113  dchrelbas4  27161  dchrinv  27179  2sqlem6  27341  chpo1ubb  27399  dchrmusumlema  27411  dchrisum0lema  27432  ostth3  27556  sltrec  27739  lrrecfr  27857  addsuniflem  27915  addsbday  27931  negsunif  27968  n0sfincut  28253  tgcgr4  28465  eqeelen  28838  brbtwn2  28839  colinearalg  28844  axcgrid  28850  axsegconlem1  28851  ax5seglem4  28866  ax5seglem5  28867  axbtwnid  28873  axpasch  28875  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem12  28909  elntg2  28919  isuvtx  29329  uvtx2vtx1edg  29332  uvtx2vtx1edgb  29333  iscplgrnb  29350  iscplgredg  29351  vdiscusgrb  29465  uhgrvd00  29469  upgriswlk  29576  wwlksnext  29830  clwwlkinwwlk  29976  clwwlkel  29982  clwwlkf  29983  clwwlkwwlksb  29990  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  clwwlknonex2lem2  30044  nmounbi  30712  blocnilem  30740  isph  30758  phoeqi  30793  h2hcau  30915  h2hlm  30916  hial2eq2  31043  hoeq1  31766  hoeq2  31767  adjsym  31769  cnvadj  31828  hhcno  31840  hhcnf  31841  adjvalval  31873  leop2  32060  leoptri  32072  mdbr2  32232  dmdbr2  32239  mddmd2  32245  cdj3lem3b  32376  infxrge0gelb  32696  prodindf  32793  toslublem  32905  tosglblem  32907  mgccnv  32932  cntrval2  33135  submarchi  33147  isarchi3  33148  lindfpropd  33360  opprlidlabs  33463  ply1moneq  33562  cmpcref  33847  lmdvg  33950  eulerpartlemd  34364  subfacp1lem3  35176  subfacp1lem5  35178  satfv1lem  35356  dfrdg2  35790  opnrebl  36315  poimirlem23  37644  broucube  37655  itg2gt0cn  37676  ftc1cnnc  37693  lmclim2  37759  caures  37761  sstotbnd2  37775  rrnmet  37830  rrncmslem  37833  isdrngo3  37960  isidlc  38016  cvrval2  39274  isat3  39307  iscvlat2N  39324  glbconN  39377  glbconNOLD  39378  ltrneq  40150  cdlemefrs29clN  40400  cdlemefrs32fva  40401  cdleme32fva  40438  cdlemk33N  40910  cdlemk34  40911  cdlemkid3N  40934  cdlemkid4  40935  diaglbN  41056  dibglbN  41167  dihglbcpreN  41301  dihglblem6  41341  hdmap1eulem  41823  hdmap1eulemOLDN  41824  hdmapoc  41932  hlhilocv  41958  primrootsunit1  42092  sn-sup3d  42487  fimgmcyc  42529  wepwsolem  43038  fnwe2lem2  43047  islnm2  43074  onmaxnelsup  43219  onsupnmax  43224  onsupuni  43225  onsupmaxb  43235  onsupeqnmax  43243  iscard5  43532  alephiso2  43554  clsk3nimkb  44036  ntrclsneine0  44061  ntrneineine0  44083  ntrneineine1  44084  ntrneicls00  44085  ntrneicls11  44086  ntrneiiso  44087  ntrneik2  44088  ntrneix2  44089  ntrneikb  44090  ntrneixb  44091  ntrneik3  44092  ntrneix3  44093  ntrneik13  44094  ntrneix13  44095  ntrneik4w  44096  ntrneik4  44097  caofcan  44319  modelac8prim  44989  infxrbnd2  45372  supminfxr  45467  rexanuz2nf  45495  evthiccabs  45501  ellimcabssub0  45622  climf  45627  clim2f  45641  clim2cf  45655  clim0cf  45659  limsupmnflem  45725  limsupre2lem  45729  limsupreuzmpt  45744  supcnvlimsup  45745  limsupge  45766  liminfreuzlem  45807  liminfltlem  45809  liminflimsupclim  45812  liminfpnfuz  45821  xlimpnfxnegmnf2  45863  fourierdlem70  46181  fourierdlem71  46182  fourierdlem73  46184  fourierdlem80  46191  fourierdlem83  46194  fourierdlem87  46198  voliunsge0lem  46477  meaiuninclem  46485  meaiuninc3v  46489  hoidmv1lelem3  46598  hoidmvlelem4  46603  hoidmvlelem5  46604  issmflem  46732  cfsetsnfsetf  47063  cfsetsnfsetfo  47065  requad2  47628  isubgrgrim  47933  grlicref  48008  islinindfis  48442  elbigolo1  48550  line2x  48747  itscnhlinecirc02p  48778  iscnrm3lem1  48926  ipolublem  48978  ipoglblem  48981  oppcup  49200  uptrlem3  49205  initopropd  49236  termopropd  49237  isinito2lem  49491  termc2  49511  lanup  49634  ranup  49635  aacllem  49794