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

Theorem ralnex2 3133
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 3072 . . 3 (∀𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑦𝐵 𝜑)
21ralbii 3093 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝐴 ¬ ∃𝑦𝐵 𝜑)
3 ralnex 3072 . 2 (∀𝑥𝐴 ¬ ∃𝑦𝐵 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
42, 3bitri 275 1 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062  df-rex 3071
This theorem is referenced by:  ralnex3  3134  r2exlem  3143  rexcom  3290  genpnnp  11045  axtgupdim2  28479  uhgrvd00  29552  nrt2irr  30492  ply1dg3rt0irred  33607  dff15  35098  fmlaomn0  35395  gonan0  35397  goaln0  35398  hashnexinj  42129  fourierdlem42  46164  ichnreuop  47459
  Copyright terms: Public domain W3C validator