Theorem dfral2 3118

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 3119. (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 3113	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑)
3		ralnex 3093	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
4	2, 3	bitri 278	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑)

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

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 3082  df-rex 3092

This theorem is used by:  rexnal  3119  rab0  4342  boxcutc  8945  infssuni  9310  ac6n  10484  indstr  12956  trfil3  24096  nosepon  27880  noinfbnd1lem4  27941  cuteq1  28061  tglowdim2ln  28976  nmobndseqi  31202  stri  32680  hstri  32688  reprinfz1  35074  bnj1204  35465  onvf1odlem4  35647  fvineqsneq  38115  poimirlem1  38329  n0elqs  39039