Theorem ralnex 3062

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2108  ∀wral 3051  ∃wrex 3060

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 3052  df-rex 3061

This theorem is referenced by:  dfrex2  3063  nrex  3064  rexim  3077  dfral2  3088  ralinexa  3090  r19.43  3108  ralnex2  3120  ralnex3  3121  nrexralim  3124  nrexdv  3135  nelb  3218  cbvrexdva  3223  cbvrexfw  3285  rexeqbidvvOLD  3316  cbvrexdva2  3328  rexeqf  3333  rexprg  4673  n0snor2el  4809  iindif2  5053  rexiunxp  5820  rexxpf  5827  f0rn0  6763  ordunisuc2  7839  tfi  7848  resf1extb  7930  releldmdifi  8044  omeulem1  8594  frfi  9293  isfinite2  9306  supmo  9464  infmo  9509  ordtypelem9  9540  elirrv  9610  unbndrank  9856  kmlem7  10171  kmlem8  10172  kmlem13  10177  isfin1-3  10400  ac6num  10493  zorn2lem4  10513  fpwwe2lem11  10655  npomex  11010  suplem2pr  11067  dedekind  11398  suprnub  12207  infregelb  12226  arch  12498  xrsupsslem  13323  xrinfmsslem  13324  supxrbnd1  13337  supxrbnd2  13338  supxrleub  13342  supxrbnd  13344  infxrgelb  13352  injresinjlem  13803  hashgt12el  14440  hashgt12el2  14441  sqrt2irr  16267  prmind2  16704  vdwnnlem3  17017  vdwnn  17018  acsfiindd  18563  isnmnd  18716  isnirred  20380  lssne0  20908  bwth  23348  t1connperf  23374  trfbas  23782  fbunfip  23807  fbasrn  23822  filuni  23823  hausflim  23919  alexsubALTlem3  23987  alexsubALTlem4  23988  ptcmplem4  23993  lebnumlem3  24913  bcthlem4  25279  bcth3  25283  amgm  26953  issqf  27098  ostth  27602  nosupbnd1lem4  27675  noinfbnd1lem4  27690  sltrec  27784  cuteq1  27798  tglowdim2ln  28630  axcontlem12  28954  umgrnloop0  29088  numedglnl  29123  usgrnloop0ALT  29184  uhgrnbgr0nb  29333  nbgr0edg  29336  vtxd0nedgb  29468  vtxdusgr0edgnelALT  29476  1hevtxdg0  29485  usgrvd0nedg  29513  uhgrvd00  29514  pthdlem2lem  29749  nmounbi  30757  lnon0  30779  largei  32248  cvbr2  32264  chrelat2i  32346  n0nsnel  32496  uniinn0  32531  infxrge0gelb  32743  nn0min  32799  toslublem  32952  tosglblem  32954  archiabl  33196  lmdvg  33984  esumcvgre  34122  eulerpartlems  34392  bnj110  34889  bnj1417  35072  lfuhgr3  35142  fmlaomn0  35412  fmla0disjsuc  35420  fmlasucdisj  35421  dfon2lem8  35808  dfint3  35970  relowlpssretop  37382  domalom  37422  fvineqsneq  37430  poimirlem26  37670  poimirlem30  37674  poimir  37677  mblfinlem1  37681  ftc1anc  37725  heiborlem1  37835  lcvbr2  39040  lcvbr3  39041  cvrnbtwn  39289  cvrval2  39292  hlrelat2  39422  cdleme0nex  40309  aks4d1p7  42096  sticksstones1  42159  infdesc  42666  nna4b4nsq  42683  rencldnfilem  42843  setindtr  43048  onmaxnelsup  43247  onsupnmax  43252  onsupmaxb  43263  onsupeqnmax  43271  ordnexbtwnsuc  43291  gneispace  44158  nelrnmpt  45108  iindif2f  45184  ralfal  45185  supxrgere  45360  supxrgelem  45364  infxrbnd2  45396  supminfxr  45491  limsupub  45733  limsuppnflem  45739  limsupre2lem  45753  stirlinglem5  46107  etransclem24  46287  etransclem32  46295  sge0iunmpt  46447  sge0rpcpnf  46450  iundjiun  46489  voliunsge0lem  46501  meaiuninc3v  46513  meaiininclem  46515  hoidmv1lelem3  46622  hoidmvlelem4  46627  hoidmvlelem5  46628  n0nsn2el  47054  0nelsetpreimafv  47404  stgr0  47972  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem2  48074  gpg5nbgrvtx13starlem3  48075  copisnmnd  48144  lindslinindsimp1  48433  lindslinindsimp2  48439  ldepslinc  48485  aacllem  49665