Theorem ralnex 3078

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 3075	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1779	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3077	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 335	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 275	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1535  ∃wex 1777   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  dfrex2  3079  nrex  3080  rexim  3093  dfral2  3105  ralinexa  3107  r19.30OLD  3127  r19.43  3128  ralnex2  3139  ralnex3  3140  nrexralim  3143  nrexdv  3155  nelb  3240  nelbOLD  3241  cbvrexdva  3246  cbvrexfw  3311  rexeqbidvvOLD  3345  cbvrexdva2  3357  rexeqf  3362  rexprg  4721  n0snor2el  4858  iindif2  5100  rexiunxp  5865  rexxpf  5872  f0rn0  6806  ordunisuc2  7881  tfi  7890  releldmdifi  8086  omeulem1  8638  frfi  9349  isfinite2  9362  supmo  9521  infmo  9564  ordtypelem9  9595  elirrv  9665  unbndrank  9911  kmlem7  10226  kmlem8  10227  kmlem13  10232  isfin1-3  10455  ac6num  10548  zorn2lem4  10568  fpwwe2lem11  10710  npomex  11065  suplem2pr  11122  dedekind  11453  suprnub  12260  infregelb  12279  arch  12550  xrsupsslem  13369  xrinfmsslem  13370  supxrbnd1  13383  supxrbnd2  13384  supxrleub  13388  supxrbnd  13390  infxrgelb  13397  injresinjlem  13837  hashgt12el  14471  hashgt12el2  14472  sqrt2irr  16297  prmind2  16732  vdwnnlem3  17044  vdwnn  17045  acsfiindd  18623  isnmnd  18776  isnirred  20446  lssne0  20972  bwth  23439  t1connperf  23465  trfbas  23873  fbunfip  23898  fbasrn  23913  filuni  23914  hausflim  24010  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem4  24084  lebnumlem3  25014  bcthlem4  25380  bcth3  25384  amgm  27052  issqf  27197  ostth  27701  nosupbnd1lem4  27774  noinfbnd1lem4  27789  sltrec  27883  cuteq1  27896  tglowdim2ln  28677  axcontlem12  29008  umgrnloop0  29144  numedglnl  29179  usgrnloop0ALT  29240  uhgrnbgr0nb  29389  nbgr0edg  29392  vtxd0nedgb  29524  vtxdusgr0edgnelALT  29532  1hevtxdg0  29541  usgrvd0nedg  29569  uhgrvd00  29570  pthdlem2lem  29803  nmounbi  30808  lnon0  30830  largei  32299  cvbr2  32315  chrelat2i  32397  n0nsnel  32544  uniinn0  32573  infxrge0gelb  32773  nn0min  32824  toslublem  32945  tosglblem  32947  archiabl  33178  lmdvg  33899  esumcvgre  34055  eulerpartlems  34325  bnj110  34834  bnj1417  35017  lfuhgr3  35087  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  dfon2lem8  35754  dfint3  35916  relowlpssretop  37330  domalom  37370  fvineqsneq  37378  poimirlem26  37606  poimirlem30  37610  poimir  37613  mblfinlem1  37617  ftc1anc  37661  heiborlem1  37771  lcvbr2  38978  lcvbr3  38979  cvrnbtwn  39227  cvrval2  39230  hlrelat2  39360  cdleme0nex  40247  aks4d1p7  42040  sticksstones1  42103  infdesc  42598  nna4b4nsq  42615  rencldnfilem  42776  setindtr  42981  onmaxnelsup  43184  onsupnmax  43189  onsupmaxb  43200  onsupeqnmax  43208  ordnexbtwnsuc  43229  gneispace  44096  nelrnmpt  44986  iindif2f  45065  ralfal  45066  supxrgere  45248  supxrgelem  45252  infxrbnd2  45284  supminfxr  45379  limsupub  45625  limsuppnflem  45631  limsupre2lem  45645  stirlinglem5  45999  etransclem24  46179  etransclem32  46187  sge0iunmpt  46339  sge0rpcpnf  46342  iundjiun  46381  voliunsge0lem  46393  meaiuninc3v  46405  meaiininclem  46407  hoidmv1lelem3  46514  hoidmvlelem4  46519  hoidmvlelem5  46520  n0nsn2el  46940  0nelsetpreimafv  47264  copisnmnd  47892  lindslinindsimp1  48186  lindslinindsimp2  48192  ldepslinc  48238  aacllem  48895