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