Theorem rexnal 3090

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

Assertion

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

Proof of Theorem rexnal

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

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

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

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

This theorem is referenced by:  r19.35  3096  r19.35OLD  3097  r19.30  3108  rexnal2  3123  rexnal3  3124  2ralorOLD  3220  raleq  3306  elpwunsn  4665  n0snor2el  4814  uni0b  4914  iundif2  5055  weniso  7352  rexrnmpo  7552  onnseq  8363  cofonr  8691  ixp0  8950  boxcutc  8960  isfinite2  9311  ordtypelem9  9545  ordtypelem10  9546  unbndrank  9861  tcrank  9903  infxpenlem  10032  kmlem3  10172  kmlem7  10176  kmlem8  10177  kmlem13  10182  cfeq0  10275  isf32lem2  10373  isf32lem5  10376  isf34lem4  10396  fin1a2lem7  10425  ac6n  10504  alephval2  10591  pwfseqlem3  10679  inttsk  10793  nqereu  10948  npomex  11015  prlem934  11052  arch  12503  qextlt  13224  qextle  13225  xralrple  13226  xrsupsslem  13328  xrinfmsslem  13329  supxrbnd1  13342  supxrbnd2  13343  supxrbnd  13349  fsuppmapnn0fiubex  14015  hashfun  14460  hashge2el2dif  14503  limsuplt  15500  fprodle  16017  alzdvds  16344  isprm5  16731  ncoprmlnprm  16752  pc2dvds  16904  vdwnn  17023  ramcl  17054  cshwshashlem1  17120  cshwshash  17129  isnsgrp  18706  isnmnd  18721  smndex1n0mnd  18895  lt6abl  19881  simpgnideld  20087  zrninitoringc  20641  psdmul  22109  mdetunilem8  22562  fctop  22947  cctop  22949  t0dist  23268  ist0-3  23288  pthaus  23581  txkgen  23595  xkohaus  23596  fbfinnfr  23784  isufil2  23851  hausflim  23924  fclscf  23968  bcth  25286  minveclem3b  25385  pmltpc  25408  volsup  25514  volsup2  25563  itg2seq  25700  itg2cn  25721  tdeglem4  26022  aaliou3lem9  26315  ftalem7  27046  dchrptlem3  27234  dchrsum2  27236  noseponlem  27633  nolt02o  27664  noetasuplem4  27705  noetainflem4  27709  cofcutr  27889  tglowdim1i  28485  tglowdim2ln  28635  brbtwn2  28889  colinearalg  28894  axlowdimlem6  28931  axlowdimlem14  28939  umgr2edg1  29195  umgr2edgneu  29198  nfrgr2v  30258  4cycl2vnunb  30276  nmounbi  30762  nmobndseqi  30765  minvecolem5  30867  fprodex01  32809  xrnarchi  33187  isarchi2  33188  ssdifidllem  33476  mxidlirred  33492  ssmxidllem  33493  fedgmullem2  33675  ordtconnlem1  33960  lmdvg  33989  hasheuni  34121  voliune  34265  volfiniune  34266  ballotlemodife  34535  ballotlem4  34536  reprdifc  34664  bnj1542  34893  bnj110  34894  bnj1189  35045  dfrecs2  35973  brub  35977  filnetlem4  36404  unblimceq0  36530  relowlpssretop  37387  nlpineqsn  37431  matunitlindflem1  37645  poimirlem23  37672  poimirlem30  37679  poimirlem32  37681  poimir  37682  mblfinlem1  37686  aks4d1p3  42096  aks4d1p8d2  42103  aks6d1c2p2  42137  aks6d1c5  42157  dffltz  42632  infdesc  42641  fphpd  42814  fiphp3d  42817  rencldnfilem  42818  pellfundglb  42883  onmaxnelsup  43222  onsupnmax  43227  ralopabb  43410  clsk3nimkb  44039  ndisj2  45055  eliin2f  45108  infrpge  45358  infxrbnd2  45376  supminfxr  45471  rexanuz2nf  45499  limcrecl  45638  limsupub  45713  limsuppnflem  45719  limsupre2lem  45733  stoweidlem14  46023  stoweidlem34  46043  salexct  46343  meaiuninc3v  46493  vonioo  46691  vonicc  46694  tworepnotupword  46895  copisnmnd  48124  pgrpgt2nabl  48321  islindeps  48409  islininds2  48440  ldepslinc  48465  line2ylem  48711  line2xlem  48713  iineq0  48778  nelsubclem  49014  setc1onsubc  49459