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

Theorem ralbidv2 2981
Description: Formula-building rule for restricted universal quantifier (deduction rule). (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 1847 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) ↔ ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 2914 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2914 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 303 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1479  wcel 1988  wral 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197  df-ral 2914
This theorem is referenced by:  ralbidva  2982  ralss  3660  oneqmini  5764  ordunisuc2  7029  dfsmo2  7429  wemapsolem  8440  zorn2lem1  9303  raluz  11721  limsupgle  14189  ello12  14228  elo12  14239  lo1resb  14276  rlimresb  14277  o1resb  14278  isprm3  15377  isprm7  15401  ist1  21106  ist1-2  21132  hausdiag  21429  xkopt  21439  cnflf  21787  cnfcf  21827  metcnp  22327  caucfil  23062  mdegleb  23805  eulerpartlemgvv  30412  filnetlem4  32351  hoidmvle  40577  elbigo2  42111
  Copyright terms: Public domain W3C validator