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

Theorem ralnex2 3258
Description: Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 18-May-2023.)
Assertion
Ref Expression
ralnex2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)

Proof of Theorem ralnex2
StepHypRef Expression
1 ralnex 3234 . . 3 (∀𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑦𝐵 𝜑)
21ralbii 3163 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝐴 ¬ ∃𝑦𝐵 𝜑)
3 ralnex 3234 . 2 (∀𝑥𝐴 ¬ ∃𝑦𝐵 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
42, 3bitri 277 1 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208  wral 3136  wrex 3137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-ral 3141  df-rex 3142
This theorem is referenced by:  ralnex3  3260  r2exlem  3300  genpnnp  10419  axtgupdim2  26249  uhgrvd00  27308  dff15  32341  fmlaomn0  32625  gonan0  32627  goaln0  32628  fourierdlem42  42419  ichnreuop  43619
  Copyright terms: Public domain W3C validator