Theorem ralnex2 3145

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

Step	Hyp	Ref	Expression
1		ralnex 3091	. . 3 ⊢ (∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 𝜑)
2	1	ralbii 3111	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ∃𝑦 ∈ 𝐵 𝜑)
3		ralnex 3091	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
4	2, 3	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3079  ∃wrex 3089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is used by:  ralnex3  3146  r2exlem  3154  rexcom  3294  genpnnp  10994  axtgupdim2  28749  prlngmolem1  29211  uhgrvd00  29893  nrt2irr  30833  ply1dg3rt0irred  33883  dff15  35481  kardexen  35584  fmlaomn0  35890  gonan0  35892  goaln0  35893  hashnexinj  42923  fourierdlem42  46891  ichnreuop  48249