MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvralvw Structured version   Visualization version   GIF version

Theorem cbvralvw 3448
Description: Version of cbvralv 3451 with a disjoint variable condition, which does not require ax-10 2139, ax-11 2154, ax-12 2170, ax-13 2384. (Contributed by Gino Giotto, 10-Jan-2024.)
Hypothesis
Ref Expression
cbvralvw.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvralvw (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralvw
StepHypRef Expression
1 eleq1w 2893 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2 cbvralvw.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2imbi12d 347 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
43cbvalvw 2037 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
5 df-ral 3141 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
6 df-ral 3141 . 2 (∀𝑦𝐴 𝜓 ↔ ∀𝑦(𝑦𝐴𝜓))
74, 5, 63bitr4i 305 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wal 1529  wcel 2108  wral 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-clel 2891  df-ral 3141
This theorem is referenced by:  cbvral2vw  3460  cbvral3vw  3462  reu7  3721  disjxun  5055  reusv3i  5295  wereu2  5545  cnvpo  6131  f1mpt  7011  dfwe2  7488  tfinds  7566  wfrlem1  7946  tfrlem1  8004  tfrlem12  8017  rdglem1  8043  tz7.48lem  8069  nneneq  8692  marypha1lem  8889  supub  8915  suplub  8916  ordtypecbv  8973  ordtypelem3  8976  ordtypelem9  8982  wemaplem1  9002  brwdom3  9038  tcrank  9305  infxpenc2  9440  aceq1  9535  aceq2  9537  dfac5  9546  dfac9  9554  dfac12lem3  9563  kmlem12  9579  kmlem14  9581  cofsmo  9683  infpssrlem4  9720  isfin3ds  9743  isf32lem2  9768  isf32lem11  9777  isf33lem  9780  domtriomlem  9856  axdc3  9868  zorn2lem7  9916  zorn2g  9917  fpwwe2cbv  10044  fpwwecbv  10058  pwfseq  10078  axgroth6  10242  dedekind  10795  suprleub  11599  infregelb  11617  nnsub  11673  uzwo  12303  ublbneg  12325  zsupss  12329  xrub  12697  fsuppmapnn0fiubex  13352  monoord2  13393  faclbnd4lem4  13648  bccl  13674  hashbc  13803  wrdind  14076  wrd2ind  14077  reuccatpfxs1  14101  cau3lem  14706  climmpt2  14922  caucvgrlem  15021  caurcvg2  15026  caucvgb  15028  fsum0diag2  15130  incexclem  15183  cvgrat  15231  mertenslem2  15233  mertens  15234  sqrt2irr  15594  gcdcllem1  15840  lcmfunsnlem1  15973  lcmfunsnlem2lem1  15974  prmind2  16021  prmpwdvds  16232  prmreclem5  16248  prmreclem6  16249  vdwlem7  16315  vdwlem10  16318  vdwlem13  16321  vdwnn  16326  ramcl  16357  isacs2  16916  catpropd  16971  grprinvlem  17875  grprinvd  17876  gsumvalx  17878  mndind  17984  issubg4  18290  isnsg2  18300  elnmz  18307  gsmsymgreqlem2  18551  psgnunilem5  18614  psgnunilem3  18616  efgsdm  18848  gsummptnn0fzfv  19099  pgpfac1lem5  19193  pgpfac1  19194  pgpfac  19198  ablfaclem3  19201  lbsextg  19926  evlslem2  20284  mpfind  20312  cply1mul  20454  mdetuni0  21222  m2cpminvid2lem  21354  mp2pm2mplem4  21409  chcoeffeqlem  21485  cayhamlem3  21487  elcls3  21683  isclo2  21688  neiptopnei  21732  tgcn  21852  subbascn  21854  txcmplem2  22242  kqfvima  22330  kqt0lem  22336  isr0  22337  r0cld  22338  regr1lem2  22340  fbun  22440  flftg  22596  fclsbas  22621  alexsubALTlem2  22648  alexsubALTlem4  22650  ptcmplem4  22655  tsmsxplem1  22753  tsmsxp  22755  ustuqtop  22847  utopsnneip  22849  prdsxmslem2  23131  isclmp  23693  iscau4  23874  caucfil  23878  iscmet3  23888  bcthlem5  23923  bcth  23924  ovolicc2lem5  24114  uniioombllem6  24181  vitali  24206  ismbf3d  24247  itg1climres  24307  itg2seq  24335  itg2monolem1  24343  itg2mono  24346  rolle  24579  dvlipcn  24583  dvivthlem1  24597  ply1divex  24722  fta1g  24753  dgrco  24857  plydivex  24878  fta1  24889  vieta1  24893  ulmcaulem  24974  ulmcau  24975  abelthlem8  25019  wilth  25640  fta  25649  dchrelbas3  25806  2sqlem6  25991  2sqlem10  25996  dchrisumlem3  26059  dchrisum  26060  dchrmusumlema  26061  dchrvmasumlema  26068  dchrisum0lema  26082  pntibndlem3  26160  pntlem3  26177  pntleml  26179  pnt3  26180  ostth2lem2  26202  ostth  26207  axcontlem1  26742  axcontlem6  26747  uspgr2wlkeq  27419  crctcshwlkn0  27591  grpoideu  28278  ubthlem3  28641  adjsym  29602  lnopunilem1  29779  elunop2  29782  lnophm  29788  cnlnadjlem5  29840  mdbr3  30066  mdbr4  30067  dmdbr3  30074  dmdbr4  30075  mddmd2  30078  fprodex01  30534  wrdt2ind  30620  toslublem  30647  tosglblem  30649  archiabl  30820  isarchiofld  30883  fedgmul  31020  qtophaus  31093  lmdvg  31189  prodindf  31275  esumcvg  31338  unelldsys  31410  ldgenpisyslem1  31415  eulerpartlemsv3  31612  eulerpartlemgvv  31627  signstfvneq0  31835  reprinfz1  31886  tgoldbachgtd  31926  bnj1185  32058  bnj222  32148  bnj517  32150  bnj1452  32317  bnj1463  32320  derangenlem  32411  subfacp1lem6  32425  subfacp1  32426  resconn  32486  cvmscbv  32498  sat1el2xp  32619  untangtr  32933  dfon2lem3  33023  dfon2lem7  33027  frpomin  33071  frrlem1  33116  nosupdm  33197  nosupbnd1lem4  33204  nosupbnd2  33209  nn0prpwlem  33663  neibastop3  33703  fnemeet2  33708  fvineqsnf1  34683  fvineqsneu  34684  pibt2  34690  phpreu  34868  poimirlem27  34911  heicant  34919  mblfinlem2  34922  ovoliunnfl  34926  voliunnfl  34928  mbfresfi  34930  upixp  34996  sdclem2  35009  fdc  35012  mettrifi  35024  heiborlem5  35085  heiborlem10  35090  heibor  35091  bfp  35094  cdleme25cv  37486  cdleme40v  37597  mzpclval  39313  dford3lem1  39614  fnwe2lem1  39641  aomclem3  39647  aomclem4  39648  aomclem8  39652  dfac11  39653  hbtlem5  39719  ntrk2imkb  40378  ntrclsk2  40409  ntrclsk4  40413  fnchoice  41277  cncmpmax  41280  wessf1ornlem  41435  disjinfi  41444  rnmptbdd  41506  rnmptbd2  41511  rnmptbd  41518  supxrunb3  41662  unb2ltle  41679  monoord2xrv  41750  uzubioo2  41835  mccl  41869  climsuse  41879  limsupre  41912  limsuppnf  41982  limsupubuz  41984  limsupmnf  41992  limsupre2  41996  limsupmnfuz  41998  limsupre2mpt  42001  limsupre3  42004  limsupre3mpt  42005  limsupre3uzlem  42006  limsupre3uz  42007  limsupreuz  42008  limsupvaluz2  42009  limsupreuzmpt  42010  climuz  42015  lmbr3  42018  limsupge  42032  liminflelimsup  42047  liminfreuz  42074  xlimpnfxnegmnf  42085  cnrefiisp  42101  xlimmnf  42112  xlimpnf  42113  xlimmnfmpt  42114  xlimpnfmpt  42115  dfxlim2  42119  dvbdfbdioolem2  42204  dvbdfbdioo  42205  ioodvbdlimc1lem1  42206  ioodvbdlimc1lem2  42207  ioodvbdlimc2lem  42209  dvnprodlem3  42223  stoweidlem7  42283  stoweidlem15  42291  stoweidlem35  42311  wallispilem3  42343  fourierdlem68  42450  fourierdlem71  42453  fourierdlem73  42455  fourierdlem87  42469  fourierdlem100  42482  fourierdlem103  42485  fourierdlem104  42486  fourierdlem107  42489  fourierdlem109  42491  fourierdlem112  42494  etransc  42559  qndenserrnbllem  42570  dfsalgen2  42615  subsaliuncl  42632  meaiuninclem  42753  ovnsubaddlem2  42844  hoidmvlelem5  42872  hoidmvle  42873  hoiqssbllem3  42897  vonioo  42955  vonicc  42958  issmf  42996  issmfle  43013  issmfgt  43024  issmfge  43037  2reuimp0  43304  uniimafveqt  43532  sbgoldbm  43940  mogoldbb  43941  bgoldbtbndlem4  43964  bgoldbtbnd  43965  nn0sumshdiglem1  44672
  Copyright terms: Public domain W3C validator