Theorem ralbidva 3150

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

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

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 3045

This theorem is referenced by:  ralbidv  3152  2ralbidva  3191  raleqbidva  3295  poinxp  5700  soinxp  5701  frinxp  5702  ordunisssuc  6415  fnmptfvd  6975  funimass3  6988  fnnfpeq0  7114  cocan1  7228  cocan2  7229  isores2  7270  isoini2  7276  ofrfvalg  7621  ofrfval2  7634  caofidlcan  7651  tfindsg2  7795  f1oweALT  7907  fnsuppres  8124  dfsmo2  8270  smores  8275  smores2  8277  dfrecs3  8295  naddunif  8611  ac6sfi  9173  fimaxg  9176  ordunifi  9179  isfinite2  9187  fipreima  9248  supisolem  9364  fiming  9390  infempty  9399  ordiso2  9407  ordtypelem7  9416  cantnf  9589  wemapwe  9593  rankval3b  9722  rankonidlem  9724  iscard  9871  acndom  9945  dfac12lem3  10040  kmlem2  10046  cflim2  10157  cfsmolem  10164  ttukeylem6  10408  alephreg  10476  suplem2pr  10947  axsup  11191  sup3  12082  infm3  12084  suprleub  12091  dfinfre  12106  infregelb  12109  ofsubeq0  12125  ofsubge0  12127  zextlt  12550  prime  12557  suprfinzcl  12590  indstr  12817  supxr2  13216  supxrbnd1  13223  supxrbnd2  13224  supxrleub  13228  supxrbnd  13230  infxrgelb  13238  fzshftral  13518  mptnn0fsupp  13904  swrdspsleq  14572  pfxeq  14602  clim  15401  rlim  15402  clim2  15411  clim2c  15412  clim0c  15414  ello1mpt  15428  lo1o1  15439  o1lo1  15444  climabs0  15492  o1compt  15494  rlimdiv  15553  geomulcvg  15783  mertenslem2  15792  mertens  15793  rpnnen2lem12  16134  sqrt2irr  16158  fprodfvdvdsd  16245  fproddvdsd  16246  dfgcd2  16457  isprm7  16619  pc11  16792  pcz  16793  1arith  16839  vdwlem8  16900  vdwlem11  16903  vdw  16906  ramval  16920  pwsle  17396  mrieqvd  17544  mreacs  17564  cidpropd  17616  ismon2  17641  monpropd  17644  isepi  17647  isepi2  17648  subsubc  17760  funcres2b  17804  funcpropd  17809  isfull2  17820  isfth2  17824  fucsect  17882  fucinv  17883  pospropd  18231  ipodrsfi  18445  tsrss  18495  grpidpropd  18536  sgrppropd  18605  mndpropd  18633  smndex1mnd  18784  grppropd  18830  issubg4  19024  gass  19180  gsmsymgrfixlem1  19306  gsmsymgreqlem2  19310  gexdvds  19463  gexdvds2  19464  subgpgp  19476  sylow3lem6  19511  efgval2  19603  efgsp1  19616  dprdf11  19904  subgdmdprd  19915  rngpropd  20059  ringpropd  20173  abvpropd  20720  lsspropd  20921  lbspropd  21003  isridlrng  21126  isridl  21159  phlpropd  21562  ishil2  21626  frlmplusgvalb  21676  frlmvscavalb  21677  frlmvplusgscavalb  21678  lindfmm  21734  islindf4  21745  islindf5  21746  assapropd  21779  psrbaglefi  21833  psrbagconf1o  21836  gsumbagdiaglem  21837  mplmonmul  21941  gsumply1eq  22194  scmatf1  22416  cpmatmcllem  22603  cpmatmcl  22604  decpmataa0  22653  decpmatmulsumfsupp  22658  pmatcollpw2lem  22662  pm2mpmhmlem1  22703  tgss2  22872  isclo  22972  neips  22998  opnnei  23005  isperf3  23038  ssidcn  23140  lmbrf  23145  cnnei  23167  cnrest2  23171  lmss  23183  lmres  23185  ist1-2  23232  ist1-3  23234  isreg2  23262  cmpfi  23293  bwth  23295  1stccn  23348  subislly  23366  kgencn  23441  ptclsg  23500  ptcnplem  23506  xkococnlem  23544  xkoinjcn  23572  tgqtop  23597  qtopcn  23599  fbflim  23861  flimrest  23868  flfnei  23876  isflf  23878  cnflf  23887  fclsopn  23899  fclsbas  23906  fclsrest  23909  isfcf  23919  cnfcf  23927  ptcmplem3  23939  tmdgsum2  23981  eltsms  24018  tsmsgsum  24024  tsmssubm  24028  tsmsf1o  24030  utopsnneiplem  24133  ismet2  24219  prdsxmetlem  24254  elmopn2  24331  prdsbl  24377  metss  24394  metrest  24410  metcnp  24427  metcnp2  24428  metcn  24429  metucn  24457  nrginvrcn  24578  metdsge  24736  divcnOLD  24755  divcn  24757  elcncf2  24781  mulc1cncf  24796  cncfmet  24800  evth2  24857  lmmbr2  25157  lmmbrf  25160  iscfil2  25164  cfil3i  25167  iscau2  25175  iscau4  25177  iscauf  25178  caucfil  25181  iscmet3lem3  25188  cfilres  25194  causs  25196  lmclim  25201  rrxmet  25306  evthicc2  25359  cniccbdd  25360  ovolfioo  25366  ovolficc  25367  ismbl2  25426  mbfsup  25563  mbfinf  25564  mbflimsup  25565  0plef  25571  mbfi1flim  25622  xrge0f  25630  itg2mulclem  25645  itgeqa  25713  ellimc2  25776  ellimc3  25778  limcflf  25780  cnlimc  25787  dvferm1  25887  dvferm2  25889  rolle  25892  dvivthlem1  25911  ftc1lem6  25946  itgsubst  25954  mdegle0  25980  deg1leb  25998  plydivex  26203  ulm2  26292  ulmcaulem  26301  ulmcau  26302  ulmdvlem3  26309  abelthlem9  26348  abelth  26349  rlimcnp  26873  ftalem3  26983  issqf  27044  sqf11  27047  mpodvdsmulf1o  27102  dvdsmulf1o  27104  dchrelbas4  27152  dchrinv  27170  2sqlem6  27332  chpo1ubb  27390  dchrmusumlema  27402  dchrisum0lema  27423  ostth3  27547  sltrec  27733  lrrecfr  27857  addsuniflem  27915  addsbday  27931  negsunif  27968  n0sfincut  28253  tgcgr4  28480  eqeelen  28853  brbtwn2  28854  colinearalg  28859  axcgrid  28865  axsegconlem1  28866  ax5seglem4  28881  ax5seglem5  28882  axbtwnid  28888  axpasch  28890  axeuclidlem  28911  axcontlem2  28914  axcontlem4  28916  axcontlem7  28919  axcontlem12  28924  elntg2  28934  isuvtx  29344  uvtx2vtx1edg  29347  uvtx2vtx1edgb  29348  iscplgrnb  29365  iscplgredg  29366  vdiscusgrb  29480  uhgrvd00  29484  upgriswlk  29590  wwlksnext  29842  clwwlkinwwlk  29988  clwwlkel  29994  clwwlkf  29995  clwwlkwwlksb  30002  wwlksext2clwwlk  30005  wwlksubclwwlk  30006  clwwlknonex2lem2  30056  nmounbi  30724  blocnilem  30752  isph  30770  phoeqi  30805  h2hcau  30927  h2hlm  30928  hial2eq2  31055  hoeq1  31778  hoeq2  31779  adjsym  31781  cnvadj  31840  hhcno  31852  hhcnf  31853  adjvalval  31885  leop2  32072  leoptri  32084  mdbr2  32244  dmdbr2  32251  mddmd2  32257  cdj3lem3b  32388  infxrge0gelb  32718  prodindf  32815  toslublem  32923  tosglblem  32925  mgccnv  32950  cntrval2  33122  submarchi  33137  isarchi3  33138  lindfpropd  33328  opprlidlabs  33431  ply1moneq  33531  cmpcref  33833  lmdvg  33936  eulerpartlemd  34350  subfacp1lem3  35175  subfacp1lem5  35177  satfv1lem  35355  dfrdg2  35789  opnrebl  36314  poimirlem23  37643  broucube  37654  itg2gt0cn  37675  ftc1cnnc  37692  lmclim2  37758  caures  37760  sstotbnd2  37774  rrnmet  37829  rrncmslem  37832  isdrngo3  37959  isidlc  38015  cvrval2  39273  isat3  39306  iscvlat2N  39323  glbconN  39376  ltrneq  40148  cdlemefrs29clN  40398  cdlemefrs32fva  40399  cdleme32fva  40436  cdlemk33N  40908  cdlemk34  40909  cdlemkid3N  40932  cdlemkid4  40933  diaglbN  41054  dibglbN  41165  dihglbcpreN  41299  dihglblem6  41339  hdmap1eulem  41821  hdmap1eulemOLDN  41822  hdmapoc  41930  hlhilocv  41956  primrootsunit1  42090  sn-sup3d  42485  fimgmcyc  42527  wepwsolem  43035  fnwe2lem2  43044  islnm2  43071  onmaxnelsup  43216  onsupnmax  43221  onsupuni  43222  onsupmaxb  43232  onsupeqnmax  43240  iscard5  43529  alephiso2  43551  clsk3nimkb  44033  ntrclsneine0  44058  ntrneineine0  44080  ntrneineine1  44081  ntrneicls00  44082  ntrneicls11  44083  ntrneiiso  44084  ntrneik2  44085  ntrneix2  44086  ntrneikb  44087  ntrneixb  44088  ntrneik3  44089  ntrneix3  44090  ntrneik13  44091  ntrneix13  44092  ntrneik4w  44093  ntrneik4  44094  caofcan  44316  modelac8prim  44986  infxrbnd2  45368  supminfxr  45463  rexanuz2nf  45491  evthiccabs  45497  ellimcabssub0  45618  climf  45623  clim2f  45637  clim2cf  45651  clim0cf  45655  limsupmnflem  45721  limsupre2lem  45725  limsupreuzmpt  45740  supcnvlimsup  45741  limsupge  45762  liminfreuzlem  45803  liminfltlem  45805  liminflimsupclim  45808  liminfpnfuz  45817  xlimpnfxnegmnf2  45859  fourierdlem70  46177  fourierdlem71  46178  fourierdlem73  46180  fourierdlem80  46187  fourierdlem83  46190  fourierdlem87  46194  voliunsge0lem  46473  meaiuninclem  46481  meaiuninc3v  46485  hoidmv1lelem3  46594  hoidmvlelem4  46599  hoidmvlelem5  46600  issmflem  46728  cfsetsnfsetf  47062  cfsetsnfsetfo  47064  requad2  47627  isubgrgrim  47933  grlicref  48016  islinindfis  48454  elbigolo1  48562  line2x  48759  itscnhlinecirc02p  48790  iscnrm3lem1  48938  ipolublem  48990  ipoglblem  48993  oppcup  49212  uptrlem3  49217  initopropd  49248  termopropd  49249  isinito2lem  49503  termc2  49523  lanup  49646  ranup  49647  aacllem  49806