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 1920 . 2 (𝜑 → (∀𝑥(𝑥𝐴𝜓) ↔ ∀𝑥(𝑥𝐵𝜒)))
3 df-ral 3062 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3062 . 2 (∀𝑥𝐵 𝜒 ↔ ∀𝑥(𝑥𝐵𝜒))
52, 3, 43bitr4g 314 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-ral 3062
This theorem is referenced by:  ralbidva  3176  raleqbidv  3346  ralssOLD  4060  oneqmini  6436  ordunisuc2  7865  dfsmo2  8387  wemapsolem  9590  zorn2lem1  10536  raluz  12938  limsupgle  15513  ello12  15552  elo12  15563  lo1resb  15600  rlimresb  15601  o1resb  15602  isprm3  16720  isprm7  16745  ist1-2  23355  hausdiag  23653  xkopt  23663  cnflf  24010  cnfcf  24050  metcnp  24554  caucfil  25317  mdegleb  26103  islinds5  33395  islbs5  33408  eulerpartlemgvv  34378  filnetlem4  36382  mnuunid  44296  iineq12dv  45111  hoidmvle  46615  elbigo2  48473  ralbidb  48720  ralbidc  48721
  Copyright terms: Public domain W3C validator