Theorem dfrex2 3059

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.)

Assertion

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

Proof of Theorem dfrex2

Step	Hyp	Ref	Expression
1		ralnex 3058	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
2	1	con2bii 357	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3047  ∃wrex 3056

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 3048  df-rex 3057

This theorem is referenced by:  rexanali  3086  r19.23v  3159  nfrexdw  3278  cbvrexf  3327  nfrexd  3339  rspcimedv  3568  rexab  3654  sbcrext  3824  cbvrexcsf  3893  rabn0  4339  r19.9rzv  4450  rexn0  4461  rexsng  4629  rexxfrd  5347  rexxfr2d  5349  rexxfrd2  5351  rexxfr  5354  rexiunxp  5780  rexxpf  5787  rexrnmptw  7028  rexrnmpt  7030  rexima  7172  cbvexfo  7224  rexrnmpo  7486  tz7.49  8364  dfsup2  9328  supnub  9346  infnlb  9377  wofib  9431  zfregs2  9623  alephval3  9998  ac6n  10373  prmreclem5  16829  sylow1lem3  19510  ordtrest2lem  23116  trfil2  23800  alexsubALTlem3  23962  alexsubALTlem4  23963  evth  24883  lhop1lem  25943  nosupbnd1lem4  27648  vdn0conngrumgrv2  30171  nmobndseqi  30754  chpssati  32338  chrelat3  32346  nn0min  32798  xrnarchi  33148  0nellinds  33330  ordtrest2NEWlem  33930  dffr5  35786  poimirlem1  37660  poimirlem26  37685  poimirlem27  37686  fdc  37784  lpssat  39051  lssat  39054  lfl1  39108  atlrelat1  39359  unxpwdom3  43127  onsupeqnmax  43279  sucomisnotcard  43576  ss2iundf  43691  zfregs2VD  44872  rext0  44970