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

Theorem cbvralw 3440
Description: Version of cbvral 3444 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.)
Hypotheses
Ref Expression
cbvralw.1 𝑦𝜑
cbvralw.2 𝑥𝜓
cbvralw.3 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvralw (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Distinct variable group:   𝑥,𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvralw
StepHypRef Expression
1 nfcv 2975 . 2 𝑥𝐴
2 nfcv 2975 . 2 𝑦𝐴
3 cbvralw.1 . 2 𝑦𝜑
4 cbvralw.2 . 2 𝑥𝜓
5 cbvralw.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvralfw 3436 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wnf 1777  wral 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-10 2138  ax-11 2153  ax-12 2169
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1774  df-nf 1778  df-sb 2063  df-clel 2891  df-nfc 2961  df-ral 3141
This theorem is referenced by:  cbvralsvw  3466  cbviin  4953  disjxun  5055  ralxpf  5710  eqfnfv2f  6799  ralrnmptw  6853  dff13f  7006  ofrfval2  7419  fmpox  7757  ovmptss  7780  cbvixp  8470  mptelixpg  8491  boxcutc  8497  xpf1o  8671  indexfi  8824  ixpiunwdom  9047  dfac8clem  9450  acni2  9464  ac6c4  9895  iundom2g  9954  uniimadomf  9959  rabssnn0fi  13346  rlim2  14845  ello1mpt  14870  o1compt  14936  fsum00  15145  iserodd  16164  pcmptdvds  16222  catpropd  16971  invfuc  17236  gsummptnn0fz  19098  gsummoncoe1  20464  gsumply1eq  20465  fiuncmp  22004  elptr2  22174  ptcld  22213  ptclsg  22215  ptcnplem  22221  cnmpt11  22263  cnmpt21  22271  ovoliunlem3  24097  ovoliun  24098  ovoliun2  24099  finiunmbl  24137  volfiniun  24140  iunmbl  24146  voliun  24147  mbfeqalem1  24234  mbfsup  24257  mbfinf  24258  mbflim  24261  itg2split  24342  itgeqa  24406  itgfsum  24419  itgabs  24427  itggt0  24434  limciun  24484  dvlipcn  24583  dvfsumlem4  24618  dvfsum2  24623  itgsubst  24638  coeeq2  24824  ulmss  24977  leibpi  25512  rlimcnp  25535  o1cxp  25544  lgamgulmlem6  25603  fsumdvdscom  25754  lgseisenlem2  25944  disjunsn  30336  bnj110  32123  bnj1529  32335  poimirlem23  34907  itgabsnc  34953  itggt0cn  34956  totbndbnd  35059  disjinfi  41443  fmptf  41498  climinff  41881  idlimc  41896  fnlimabslt  41949  limsupref  41955  limsupbnd1f  41956  climbddf  41957  climinf2  41977  limsupubuz  41983  climinfmpt  41985  limsupmnf  41991  limsupre2  41995  limsupmnfuz  41997  limsupre3  42003  limsupre3uz  42006  limsupreuz  42007  climuz  42014  lmbr3  42017  limsupgt  42048  liminfreuz  42073  liminflt  42075  xlimpnfxnegmnf  42084  xlimmnf  42111  xlimpnf  42112  dfxlim2  42118  cncfshift  42146  stoweidlem31  42306  iundjiun  42732  meaiunincf  42755  pimgtmnf2  42982  smfpimcc  43072
  Copyright terms: Public domain W3C validator