Theorem dfral2 3164

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

Assertion

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

Proof of Theorem dfral2

Step	Hyp	Ref	Expression
1		notnotb 314	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	ralbii 3090	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑)
3		ralnex 3163	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
4	2, 3	bitri 274	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3063  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexnal  3165  boxcutc  8687  infssuni  9040  ac6n  10172  indstr  12585  trfil3  22947  tglowdim2ln  26916  nmobndseqi  29042  stri  30520  hstri  30528  reprinfz1  32502  bnj1204  32892  imaeqsalv  33594  nosepon  33795  noinfbnd1lem4  33856  fvineqsneq  35510  poimirlem1  35705  n0elqs  36388