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

Theorem ralbidv2 3172
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 1918 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) ↔ ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3060 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3060 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 314 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535  wcel 2106  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908
This theorem depends on definitions:  df-bi 207  df-ral 3060
This theorem is referenced by:  ralbidva  3174  raleqbidv  3344  ralss  4070  oneqmini  6438  ordunisuc2  7865  dfsmo2  8386  wemapsolem  9588  zorn2lem1  10534  raluz  12936  limsupgle  15510  ello12  15549  elo12  15560  lo1resb  15597  rlimresb  15598  o1resb  15599  isprm3  16717  isprm7  16742  ist1-2  23371  hausdiag  23669  xkopt  23679  cnflf  24026  cnfcf  24066  metcnp  24570  caucfil  25331  mdegleb  26118  islinds5  33375  islbs5  33388  eulerpartlemgvv  34358  filnetlem4  36364  mnuunid  44273  iineq12dv  45046  hoidmvle  46556  elbigo2  48402  ralbidb  48649  ralbidc  48650
  Copyright terms: Public domain W3C validator