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

Theorem ralnex2 3131
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 3070 . . 3 (∀𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑦𝐵 𝜑)
21ralbii 3091 . 2 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑥𝐴 ¬ ∃𝑦𝐵 𝜑)
3 ralnex 3070 . 2 (∀𝑥𝐴 ¬ ∃𝑦𝐵 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
42, 3bitri 275 1 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wral 3059  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069
This theorem is referenced by:  ralnex3  3132  r2exlem  3141  rexcom  3288  genpnnp  11043  axtgupdim2  28494  uhgrvd00  29567  nrt2irr  30502  ply1dg3rt0irred  33587  dff15  35077  fmlaomn0  35375  gonan0  35377  goaln0  35378  hashnexinj  42110  fourierdlem42  46105  ichnreuop  47397
  Copyright terms: Public domain W3C validator