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

Theorem ralbidv2 3174
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.)
Hypothesis
Ref Expression
ralbidv2.1 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
Assertion
Ref Expression
ralbidv2 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem ralbidv2
StepHypRef Expression
1 ralbidv2.1 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
21albidv 1924 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) ↔ ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3063 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3063 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 314 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  wcel 2107  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ral 3063
This theorem is referenced by:  ralbidva  3176  raleqbidv  3343  ralss  4055  oneqmini  6417  ordunisuc2  7833  dfsmo2  8347  wemapsolem  9545  zorn2lem1  10491  raluz  12880  limsupgle  15421  ello12  15460  elo12  15471  lo1resb  15508  rlimresb  15509  o1resb  15510  isprm3  16620  isprm7  16645  ist1-2  22851  hausdiag  23149  xkopt  23159  cnflf  23506  cnfcf  23546  metcnp  24050  caucfil  24800  mdegleb  25582  islinds5  32480  islbs5  32496  eulerpartlemgvv  33375  filnetlem4  35266  mnuunid  43036  hoidmvle  45316  elbigo2  47238  ralbidb  47485  ralbidc  47486
  Copyright terms: Public domain W3C validator