Theorem dfral2 3085

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 3086. (Revised by Wolf Lammen, 9-Dec-2019.)

Assertion

Ref	Expression
dfral2	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)

Proof of Theorem dfral2

Step	Hyp	Ref	Expression
1		notnotb 315	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	ralbii 3080	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑)
3		ralnex 3060	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
4	2, 3	bitri 275	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3049  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3050  df-rex 3059

This theorem is referenced by:  rexnal  3086  imaeqsalvOLD  7308  boxcutc  8877  infssuni  9244  ac6n  10393  indstr  12827  trfil3  23830  nosepon  27631  noinfbnd1lem4  27692  cuteq1  27805  tglowdim2ln  28672  nmobndseqi  30803  stri  32281  hstri  32289  reprinfz1  34728  bnj1204  35117  onvf1odlem4  35249  fvineqsneq  37556  poimirlem1  37761  n0elqs  38464