Theorem dfral2 3088

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3051  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3052  df-rex 3062

This theorem is referenced by:  rexnal  3089  imaeqsalvOLD  7319  boxcutc  8889  infssuni  9256  ac6n  10407  indstr  12866  trfil3  23853  nosepon  27629  noinfbnd1lem4  27690  cuteq1  27809  tglowdim2ln  28719  nmobndseqi  30850  stri  32328  hstri  32336  reprinfz1  34766  bnj1204  35154  onvf1odlem4  35288  fvineqsneq  37728  poimirlem1  37942  n0elqs  38653