Theorem ralnex 3065

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by BJ, 16-Jul-2021.)

Assertion

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

Proof of Theorem ralnex

Step	Hyp	Ref	Expression
1		raln 3062	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1788	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3064	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 336	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 276	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396  ∀wal 1545  ∃wex 1786   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3054  df-rex 3064

This theorem is referenced by:  dfrex2  3066  nrex  3067  rexim  3080  dfral2  3090  ralinexa  3092  r19.43  3107  ralnex2  3119  ralnex3  3120  nrexralim  3123  nrexdv  3134  nelb  3215  cbvrexdva  3220  cbvrexfw  3280  cbvrexdva2  3316  rexeqf  3321  rexprg  4629  n0snor2el  4764  iindif2  5006  rexiunxp  5782  rexxpf  5789  nelrnmpt  5909  f0rn0  6712  ordunisuc2  7784  tfi  7793  resf1extb  7874  releldmdifi  7987  omeulem1  8507  frfi  9185  isfinite2  9198  supmo  9355  infmo  9400  ordtypelem9  9431  elirrvOLDOLD  9504  unbndrank  9757  kmlem7  10070  kmlem8  10071  kmlem13  10076  isfin1-3  10299  ac6num  10392  zorn2lem4  10412  fpwwe2lem11  10555  npomex  10910  suplem2pr  10967  dedekind  11300  suprnub  12112  infregelb  12131  arch  12425  xrsupsslem  13250  xrinfmsslem  13251  supxrbnd1  13264  supxrbnd2  13265  supxrleub  13269  supxrbnd  13271  infxrgelb  13279  injresinjlem  13736  hashgt12el  14375  hashgt12el2  14376  sqrt2irr  16207  prmind2  16645  vdwnnlem3  16959  vdwnn  16960  acsfiindd  18510  isnmnd  18697  isnirred  20391  lssne0  20941  bwth  23393  t1connperf  23419  trfbas  23827  fbunfip  23852  fbasrn  23867  filuni  23868  hausflim  23964  alexsubALTlem3  24032  alexsubALTlem4  24033  ptcmplem4  24038  lebnumlem3  24948  bcthlem4  25312  bcth3  25316  amgm  26972  issqf  27117  ostth  27620  nosupbnd1lem4  27693  noinfbnd1lem4  27708  ltsrec  27811  cuteq1  27827  tglowdim2ln  28737  axcontlem12  29062  umgrnloop0  29196  numedglnl  29231  usgrnloop0ALT  29292  uhgrnbgr0nb  29441  nbgr0edg  29444  vtxd0nedgb  29575  vtxdusgr0edgnelALT  29583  1hevtxdg0  29592  usgrvd0nedg  29620  uhgrvd00  29621  pthdlem2lem  29853  nmounbi  30865  lnon0  30887  largei  32356  cvbr2  32372  chrelat2i  32454  n0nsnel  32603  uniinn0  32639  infxrge0gelb  32858  nn0min  32913  toslublem  33051  tosglblem  33053  archiabl  33279  lmdvg  34137  esumcvgre  34275  eulerpartlems  34544  bnj110  35040  bnj1417  35223  fineqvnttrclselem1  35302  lfuhgr3  35348  fmlaomn0  35618  fmla0disjsuc  35626  fmlasucdisj  35627  dfon2lem8  36016  dfint3  36180  bj-axseprep  37427  relowlpssretop  37726  domalom  37766  fvineqsneq  37774  poimirlem26  38013  poimirlem30  38017  poimir  38020  mblfinlem1  38024  ftc1anc  38068  heiborlem1  38178  lcvbr2  39514  lcvbr3  39515  cvrnbtwn  39763  cvrval2  39766  hlrelat2  39895  cdleme0nex  40782  aks4d1p7  42568  sticksstones1  42631  infdesc  43093  nna4b4nsq  43110  rencldnfilem  43265  setindtr  43469  onmaxnelsup  43668  onsupnmax  43673  onsupmaxb  43684  onsupeqnmax  43692  ordnexbtwnsuc  43712  gneispace  44578  iindif2f  45607  ralfal  45608  supxrgere  45778  supxrgelem  45782  infxrbnd2  45813  supminfxr  45907  limsupub  46147  limsuppnflem  46153  limsupre2lem  46167  stirlinglem5  46521  etransclem24  46701  etransclem32  46709  sge0iunmpt  46861  sge0rpcpnf  46864  iundjiun  46903  voliunsge0lem  46915  meaiuninc3v  46927  meaiininclem  46929  hoidmv1lelem3  47036  hoidmvlelem4  47041  hoidmvlelem5  47042  n0nsn2el  47488  0nelsetpreimafv  47865  nprmmul1  48002  stgr0  48451  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg5edgnedg  48621  copisnmnd  48660  lindslinindsimp1  48948  lindslinindsimp2  48954  ldepslinc  49000  aacllem  50291