Theorem dfral2 3117

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

Assertion

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

Proof of Theorem dfral2

Step	Hyp	Ref	Expression
1		notnotb 318	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	ralbii 3112	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑)
3		ralnex 3092	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
4	2, 3	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081  df-rex 3091

This theorem is used by:  rexnal  3118  rab0  4338  boxcutc  9007  infssuni  9373  ac6n  10602  indstr  13083  trfil3  24262  nosepon  28079  noinfbnd1lem4  28140  cuteq1  28260  tglowdim2ln  29177  nmobndseqi  31438  stri  32916  hstri  32924  reprinfz1  35362  bnj1204  35753  onvf1odlem4  36075  fvineqsneq  38603  poimirlem1  38807  n0elqs  39530