Theorem ralnex 3174

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 3173	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		alnex 1825	. . 3 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3096	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4	2, 3	xchbinxr 327	. 2 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	1, 4	bitri 267	1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 386  ∀wal 1599  ∃wex 1823   ∈ wcel 2107  ∀wral 3090  ∃wrex 3091

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-ral 3095  df-rex 3096

This theorem is referenced by:  dfral2  3175  dfrex2  3177  ralinexa  3178  nrexralim  3180  nrex  3181  nrexdv  3182  ralnex2  3228  ralnex3  3230  r19.43  3279  n0snor2el  4593  iindif2  4822  rexiunxp  5508  rexxpf  5515  f0rn0  6340  ordunisuc2  7322  tfi  7331  omeulem1  7946  frfi  8493  isfinite2  8506  supmo  8646  infmo  8689  ordtypelem9  8720  elirrv  8790  unbndrank  9002  kmlem7  9313  kmlem8  9314  kmlem13  9319  isfin1-3  9543  ac6num  9636  zorn2lem4  9656  fpwwe2lem12  9798  npomex  10153  suplem2pr  10210  dedekind  10539  suprnub  11342  infregelb  11361  arch  11639  xrsupsslem  12449  xrinfmsslem  12450  supxrbnd1  12463  supxrbnd2  12464  supxrleub  12468  supxrbnd  12470  infxrgelb  12477  injresinjlem  12907  hashgt12el  13524  hashgt12el2  13525  sqrt2irr  15382  prmind2  15803  vdwnnlem3  16105  vdwnn  16106  acsfiindd  17563  isnmnd  17684  isnirred  19087  lssne0  19343  bwth  21622  t1connperf  21648  trfbas  22056  fbunfip  22081  fbasrn  22096  filuni  22097  hausflim  22193  alexsubALTlem3  22261  alexsubALTlem4  22262  ptcmplem4  22267  lebnumlem3  23170  bcthlem4  23533  bcth3  23537  amgm  25169  issqf  25314  ostth  25780  tglowdim2ln  26002  axcontlem12  26324  umgrnloop0  26457  numedglnl  26493  usgrnloop0ALT  26551  uhgrnbgr0nb  26701  nbgr0edg  26704  vtxd0nedgb  26836  vtxdusgr0edgnelALT  26844  1hevtxdg0  26853  usgrvd0nedg  26881  uhgrvd00  26882  pthdlem2lem  27119  nmounbi  28203  lnon0  28225  largei  29698  cvbr2  29714  chrelat2i  29796  uniinn0  29929  infxrge0gelb  30096  nn0min  30131  toslublem  30229  tosglblem  30231  archiabl  30314  lmdvg  30597  esumcvgre  30751  eulerpartlems  31020  bnj110  31527  bnj1417  31708  dfon2lem8  32283  nosupbnd1lem4  32446  sltrec  32513  dfint3  32648  unblimceq0  33080  relowlpssretop  33807  poimirlem26  34063  poimirlem30  34067  poimir  34070  mblfinlem1  34074  ftc1anc  34120  heiborlem1  34236  lcvbr2  35178  lcvbr3  35179  cvrnbtwn  35427  cvrval2  35430  hlrelat2  35559  cdleme0nex  36446  rencldnfilem  38348  setindtr  38554  gneispace  39392  nelrnmpt  40192  supxrgere  40461  supxrgelem  40465  infxrbnd2  40497  supminfxr  40603  limsupub  40848  limsuppnflem  40854  limsupre2lem  40868  stirlinglem5  41226  etransclem24  41406  etransclem32  41414  sge0iunmpt  41563  sge0rpcpnf  41566  iundjiun  41605  voliunsge0lem  41617  meaiuninc3v  41629  meaiininclem  41631  hoidmv1lelem3  41738  hoidmvlelem4  41743  hoidmvlelem5  41744  copisnmnd  42828  lindslinindsimp1  43265  lindslinindsimp2  43271  ldepslinc  43317  aacllem  43657