Theorem ralnex 3073

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397  ∀wal 1540  ∃wex 1782   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063  df-rex 3072

This theorem is referenced by:  dfrex2  3074  nrex  3075  rexim  3088  dfral2  3100  ralinexa  3102  r19.30OLD  3122  r19.43  3123  ralnex2  3134  ralnex3  3135  nrexralim  3138  nrexdv  3150  nelb  3232  nelbOLD  3233  cbvrexdva  3238  cbvrexfw  3303  rexeqbidvvOLD  3333  cbvrexdva2  3346  rexeqf  3351  rexprg  4701  n0snor2el  4835  iindif2  5081  rexiunxp  5841  rexxpf  5848  f0rn0  6777  ordunisuc2  7833  tfi  7842  releldmdifi  8031  omeulem1  8582  frfi  9288  isfinite2  9301  supmo  9447  infmo  9490  ordtypelem9  9521  elirrv  9591  unbndrank  9837  kmlem7  10151  kmlem8  10152  kmlem13  10157  isfin1-3  10381  ac6num  10474  zorn2lem4  10494  fpwwe2lem11  10636  npomex  10991  suplem2pr  11048  dedekind  11377  suprnub  12179  infregelb  12198  arch  12469  xrsupsslem  13286  xrinfmsslem  13287  supxrbnd1  13300  supxrbnd2  13301  supxrleub  13305  supxrbnd  13307  infxrgelb  13314  injresinjlem  13752  hashgt12el  14382  hashgt12el2  14383  sqrt2irr  16192  prmind2  16622  vdwnnlem3  16930  vdwnn  16931  acsfiindd  18506  isnmnd  18629  isnirred  20234  lssne0  20561  bwth  22914  t1connperf  22940  trfbas  23348  fbunfip  23373  fbasrn  23388  filuni  23389  hausflim  23485  alexsubALTlem3  23553  alexsubALTlem4  23554  ptcmplem4  23559  lebnumlem3  24479  bcthlem4  24844  bcth3  24848  amgm  26495  issqf  26640  ostth  27142  nosupbnd1lem4  27214  noinfbnd1lem4  27229  sltrec  27321  cuteq1  27334  tglowdim2ln  27902  axcontlem12  28233  umgrnloop0  28369  numedglnl  28404  usgrnloop0ALT  28462  uhgrnbgr0nb  28611  nbgr0edg  28614  vtxd0nedgb  28745  vtxdusgr0edgnelALT  28753  1hevtxdg0  28762  usgrvd0nedg  28790  uhgrvd00  28791  pthdlem2lem  29024  nmounbi  30029  lnon0  30051  largei  31520  cvbr2  31536  chrelat2i  31618  uniinn0  31782  infxrge0gelb  31979  nn0min  32026  toslublem  32142  tosglblem  32144  archiabl  32344  lmdvg  32933  esumcvgre  33089  eulerpartlems  33359  bnj110  33869  bnj1417  34052  lfuhgr3  34110  fmlaomn0  34381  fmla0disjsuc  34389  fmlasucdisj  34390  dfon2lem8  34762  dfint3  34924  relowlpssretop  36245  domalom  36285  fvineqsneq  36293  poimirlem26  36514  poimirlem30  36518  poimir  36521  mblfinlem1  36525  ftc1anc  36569  heiborlem1  36679  lcvbr2  37892  lcvbr3  37893  cvrnbtwn  38141  cvrval2  38144  hlrelat2  38274  cdleme0nex  39161  aks4d1p7  40948  sticksstones1  40962  infdesc  41385  nna4b4nsq  41402  rencldnfilem  41558  setindtr  41763  onmaxnelsup  41972  onsupnmax  41977  onsupmaxb  41988  onsupeqnmax  41996  ordnexbtwnsuc  42017  gneispace  42885  nelrnmpt  43773  iindif2f  43854  ralfal  43855  supxrgere  44043  supxrgelem  44047  infxrbnd2  44079  supminfxr  44174  limsupub  44420  limsuppnflem  44426  limsupre2lem  44440  stirlinglem5  44794  etransclem24  44974  etransclem32  44982  sge0iunmpt  45134  sge0rpcpnf  45137  iundjiun  45176  voliunsge0lem  45188  meaiuninc3v  45200  meaiininclem  45202  hoidmv1lelem3  45309  hoidmvlelem4  45314  hoidmvlelem5  45315  n0nsn2el  45735  0nelsetpreimafv  46058  copisnmnd  46579  lindslinindsimp1  47138  lindslinindsimp2  47144  ldepslinc  47190  aacllem  47848