Theorem ralbidva 3183

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077

This theorem is used by:  ralbidv  3185  2ralbidva  3224  raleqbidva  3325  poinxp  5728  soinxp  5729  frinxp  5730  ordunisssuc  6460  fnmptfvd  7028  funimass3  7041  fnnfpeq0  7171  cocan1  7287  cocan2  7288  isores2  7329  isoini2  7335  ofrfvalg  7684  ofrfval2  7697  caofidlcan  7714  tfindsg2  7856  f1oweALT  7967  fnsuppres  8186  dfsmo2  8333  smores  8338  smores2  8340  dfrecs3  8358  naddunif  8681  ac6sfi  9253  fimaxg  9256  ordunifi  9259  isfinite2  9268  fipreima  9325  supisolem  9444  fiming  9470  infempty  9479  ordiso2  9487  ordtypelem7  9496  cantnf  9672  wemapwe  9676  rankval3b  9809  rankonidlem  9811  iscard  10027  acndom  10101  dfac12lem3  10195  kmlem2  10201  cflim2  10312  cfsmolem  10319  ttukeylem6  10563  alephreg  10638  suplem2pr  11109  axsup  11356  sup3  12243  infm3  12245  suprleub  12252  dfinfre  12267  infregelb  12270  ofsubeq0  12286  ofsubge0  12288  zextlt  12742  prime  12749  suprfinzcl  12782  indstr  13012  supxr2  13413  supxrbnd1  13420  supxrbnd2  13421  supxrleub  13425  supxrbnd  13427  infxrgelb  13435  fzshftral  13717  mptnn0fsupp  14108  swrdspsleq  14782  pfxeq  14812  clim  15628  rlim  15629  clim2  15638  clim2c  15639  clim0c  15641  ello1mpt  15655  lo1o1  15666  o1lo1  15671  climabs0  15719  o1compt  15721  rlimdiv  15780  geomulcvg  16012  mertenslem2  16021  mertens  16022  rpnnen2lem12  16360  sqrt2irr  16384  fprodfvdvdsd  16471  fproddvdsd  16472  dfgcd2  16683  isprm7  16846  pc11  17019  pcz  17020  1arith  17066  vdwlem8  17127  vdwlem11  17130  vdw  17133  ramval  17147  pwsle  17625  mrieqvd  17773  mreacs  17793  cidpropd  17845  ismon2  17870  monpropd  17873  isepi  17876  isepi2  17877  subsubc  17989  funcres2b  18033  funcpropd  18038  isfull2  18049  isfth2  18053  fucsect  18111  fucinv  18112  pospropd  18460  ipodrsfi  18674  tsrss  18724  grpidpropd  18803  mgmidpfod  18818  sgrppropd  18881  mndpropd  18912  smndex1mnd  19070  grppropd  19123  issubg4  19317  gass  19476  gsmsymgrfixlem1  19602  gsmsymgreqlem2  19606  gexdvds  19759  gexdvds2  19760  subgpgp  19772  sylow3lem6  19807  efgval2  19899  efgsp1  19912  dprdf11  20200  subgdmdprd  20211  rngpropd  20357  ringpropd  20480  isdrng5  20969  abvpropd  21053  lsspropd  21253  lbspropd  21335  isridlrng  21459  isridl  21506  phlpropd  21922  ishil2  21986  frlmplusgvalb  22036  frlmvscavalb  22037  frlmvplusgscavalb  22038  lindfmm  22094  islindf4  22105  islindf5  22106  assapropd  22140  psrbaglefi  22195  psrbagconf1o  22198  gsumbagdiaglem  22200  mplmonmul  22306  gsumply1eq  22588  scmatf1  22807  cpmatmcllem  22997  cpmatmcl  22998  decpmataa0  23047  decpmatmulsumfsupp  23052  pmatcollpw2lem  23056  pm2mpmhmlem1  23097  tgss2  23266  isclo  23366  neips  23392  opnnei  23399  isperf3  23432  ssidcn  23534  lmbrf  23539  cnnei  23561  cnrest2  23565  lmss  23577  lmres  23579  ist1-2  23626  ist1-3  23628  isreg2  23656  cmpfi  23687  bwth  23689  1stccn  23743  subislly  23761  kgencn  23836  ptclsg  23895  ptcnplem  23901  xkococnlem  23939  xkoinjcn  23967  tgqtop  23992  qtopcn  23994  fbflim  24256  flimrest  24263  flfnei  24271  isflf  24273  cnflf  24282  fclsopn  24294  fclsbas  24301  fclsrest  24304  isfcf  24314  cnfcf  24322  ptcmplem3  24334  tmdgsum2  24376  eltsms  24413  tsmsgsum  24419  tsmssubm  24423  tsmsf1o  24425  utopsnneiplem  24527  ismet2  24613  prdsxmetlem  24648  elmopn2  24725  prdsbl  24771  metss  24788  metrest  24804  metcnp  24821  metcnp2  24822  metcn  24823  metucn  24851  nrginvrcn  24972  metdsge  25130  divcn  25150  elcncf2  25172  mulc1cncf  25187  cncfmet  25191  evth2  25242  lmmbr2  25541  lmmbrf  25544  iscfil2  25548  cfil3i  25551  iscau2  25559  iscau4  25561  iscauf  25562  caucfil  25565  iscmet3lem3  25572  cfilres  25578  causs  25580  lmclim  25585  rrxmet  25690  evthicc2  25742  cniccbdd  25743  ovolfioo  25749  ovolficc  25750  ismbl2  25809  mbfsup  25946  mbfinf  25947  mbflimsup  25948  0plef  25954  mbfi1flim  26005  xrge0f  26013  itg2mulclem  26028  itgeqa  26095  ellimc2  26158  ellimc3  26160  limcflf  26162  cnlimc  26169  dvferm1  26266  dvferm2  26268  rolle  26271  dvivthlem1  26289  ftc1lem6  26322  itgsubst  26330  mdegle0  26356  deg1leb  26374  plydivex  26581  rnplynfin  26593  ulm2  26675  ulmcaulem  26684  ulmcau  26685  ulmdvlem3  26692  abelthlem9  26730  abelth  26731  rlimcnp  27256  ftalem3  27365  issqf  27426  sqf11  27429  mpodvdsmulf1o  27484  dvdsmulf1o  27486  dchrelbas4  27533  dchrinv  27551  2sqlem6  27713  chpo1ubb  27771  dchrmusumlema  27783  dchrisum0lema  27804  ostth3  27928  ltsrec  28120  lrrecfr  28262  addsuniflem  28320  addbday  28337  negsunif  28374  n0fincut  28674  bdayfinbndlem1  28786  elreno2  28814  tgcgr4  28927  eqeelen  29415  brbtwn2  29416  colinearalg  29421  axcgrid  29427  axsegconlem1  29428  ax5seglem4  29443  ax5seglem5  29444  axbtwnid  29450  axpasch  29452  axeuclidlem  29473  axcontlem2  29476  axcontlem4  29478  axcontlem7  29481  axcontlem12  29486  elntg2  29496  isuvtx  29909  uvtx2vtx1edg  29912  uvtx2vtx1edgb  29913  iscplgrnb  29930  iscplgredg  29931  vdiscusgrb  30044  uhgrvd00  30048  upgriswlk  30154  wwlksnext  30415  clwwlkinwwlk  30564  clwwlkel  30570  clwwlkf  30571  clwwlkwwlksb  30578  wwlksext2clwwlk  30581  wwlksubclwwlk  30582  clwwlknonex2lem2  30632  nmounbi  31311  blocnilem  31339  isph  31357  phoeqi  31392  h2hcau  31514  h2hlm  31515  hial2eq2  31642  hoeq1  32365  hoeq2  32366  adjsym  32368  cnvadj  32427  hhcno  32439  hhcnf  32440  adjvalval  32472  leop2  32659  leoptri  32671  mdbr2  32831  dmdbr2  32838  mddmd2  32844  cdj3lem3b  32975  infxrge0gelb  33291  prodindf  33362  toslublem  33466  tosglblem  33468  mgccnv  33493  cntrval2  33665  submarchi  33680  isarchi3  33681  lindfpropd  33870  opprlidlabs  33942  ply1moneq  34053  psrmonmul  34115  cmpcref  34415  lmdvg  34518  eulerpartlemd  34932  subfacp1lem3  35868  subfacp1lem5  35870  satfv1lem  36048  dfrdg2  36479  nadddilem2  36892  nadddilem4  36894  opnrebl  37030  poimirlem23  38481  broucube  38492  itg2gt0cn  38513  ftc1cnnc  38530  lmclim2  38612  caures  38614  sstotbnd2  38628  rrnmet  38683  rrncmslem  38686  isdrngo3  38813  isidlc  38869  cvrval2  40251  isat3  40284  iscvlat2N  40301  glbconN  40354  ltrneq  41126  cdlemefrs29clN  41376  cdlemefrs32fva  41377  cdleme32fva  41414  cdlemk33N  41886  cdlemk34  41887  cdlemkid3N  41910  cdlemkid4  41911  diaglbN  42032  dibglbN  42143  dihglbcpreN  42277  dihglblem6  42317  hdmap1eulem  42799  hdmap1eulemOLDN  42800  hdmapoc  42908  hlhilocv  42934  primrootsunit1  43067  sn-sup3d  43484  fimgmcyc  43520  wepwsolem  43987  fnwe2lem2  43996  islnm2  44023  onmaxnelsup  44168  onsupnmax  44173  onsupuni  44174  onsupmaxb  44184  onsupeqnmax  44192  iscard5  44480  alephiso2  44502  clsk3nimkb  44984  ntrclsneine0  45009  ntrneineine0  45031  ntrneineine1  45032  ntrneicls00  45033  ntrneicls11  45034  ntrneiiso  45035  ntrneik2  45036  ntrneix2  45037  ntrneikb  45038  ntrneixb  45039  ntrneik3  45040  ntrneix3  45041  ntrneik13  45042  ntrneix13  45043  ntrneik4w  45044  ntrneik4  45045  caofcan  45251  modelac8prim  45919  infxrbnd2  46302  supminfxr  46396  rexanuz2nf  46424  evthiccabs  46430  ellimcabssub0  46551  climf  46556  clim2f  46568  clim2cf  46582  clim0cf  46586  limsupmnflem  46652  limsupre2lem  46656  limsupreuzmpt  46671  supcnvlimsup  46672  limsupge  46693  liminfreuzlem  46734  liminfltlem  46736  liminflimsupclim  46739  liminfpnfuz  46748  xlimpnfxnegmnf2  46790  fourierdlem70  47108  fourierdlem71  47109  fourierdlem73  47111  fourierdlem80  47118  fourierdlem83  47121  fourierdlem87  47125  voliunsge0lem  47404  meaiuninclem  47412  meaiuninc3v  47416  hoidmv1lelem3  47525  hoidmvlelem4  47530  hoidmvlelem5  47531  issmflem  47659  chnerlem1  47814  cfsetsnfsetf  48050  cfsetsnfsetfo  48052  nprmmul1  48531  requad2  48643  isubgrgrim  48949  grlicref  49032  islinindfis  49483  elbigolo1  49591  line2x  49788  itscnhlinecirc02p  49819  iscnrm3lem1  49964  ipolublem  50016  ipoglblem  50019  oppcup  50237  uptrlem3  50242  initopropd  50273  termopropd  50274  isinito2lem  50528  termc2  50548  lanup  50671  ranup  50672  aacllem  50861