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

Theorem ralbidv2 3200
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 1914 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) ↔ ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3148 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3148 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 315 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1528  wcel 2107  wral 3143
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
This theorem depends on definitions:  df-bi 208  df-ral 3148
This theorem is referenced by:  ralbidva  3201  raleqbidv  3407  ralss  4041  oneqmini  6240  ordunisuc2  7547  dfsmo2  7975  wemapsolem  9003  zorn2lem1  9907  raluz  12285  limsupgle  14824  ello12  14863  elo12  14874  lo1resb  14911  rlimresb  14912  o1resb  14913  isprm3  16017  isprm7  16042  ist1-2  21874  hausdiag  22172  xkopt  22182  cnflf  22529  cnfcf  22569  metcnp  23069  caucfil  23804  mdegleb  24576  islinds5  30849  eulerpartlemgvv  31523  filnetlem4  33616  mnuunid  40481  hoidmvle  42751  elbigo2  44447
  Copyright terms: Public domain W3C validator