Theorem ralnex 3070

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1535  ∃wex 1776   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069

This theorem is referenced by:  dfrex2  3071  nrex  3072  rexim  3085  dfral2  3097  ralinexa  3099  r19.30OLD  3119  r19.43  3120  ralnex2  3131  ralnex3  3132  nrexralim  3135  nrexdv  3147  nelb  3232  nelbOLD  3233  cbvrexdva  3238  cbvrexfw  3303  rexeqbidvvOLD  3335  cbvrexdva2  3347  rexeqf  3352  rexprg  4702  n0snor2el  4838  iindif2  5082  rexiunxp  5854  rexxpf  5861  f0rn0  6794  ordunisuc2  7865  tfi  7874  releldmdifi  8069  omeulem1  8619  frfi  9319  isfinite2  9332  supmo  9490  infmo  9533  ordtypelem9  9564  elirrv  9634  unbndrank  9880  kmlem7  10195  kmlem8  10196  kmlem13  10201  isfin1-3  10424  ac6num  10517  zorn2lem4  10537  fpwwe2lem11  10679  npomex  11034  suplem2pr  11091  dedekind  11422  suprnub  12231  infregelb  12250  arch  12521  xrsupsslem  13346  xrinfmsslem  13347  supxrbnd1  13360  supxrbnd2  13361  supxrleub  13365  supxrbnd  13367  infxrgelb  13374  injresinjlem  13823  hashgt12el  14458  hashgt12el2  14459  sqrt2irr  16282  prmind2  16719  vdwnnlem3  17031  vdwnn  17032  acsfiindd  18611  isnmnd  18764  isnirred  20437  lssne0  20967  bwth  23434  t1connperf  23460  trfbas  23868  fbunfip  23893  fbasrn  23908  filuni  23909  hausflim  24005  alexsubALTlem3  24073  alexsubALTlem4  24074  ptcmplem4  24079  lebnumlem3  25009  bcthlem4  25375  bcth3  25379  amgm  27049  issqf  27194  ostth  27698  nosupbnd1lem4  27771  noinfbnd1lem4  27786  sltrec  27880  cuteq1  27893  tglowdim2ln  28674  axcontlem12  29005  umgrnloop0  29141  numedglnl  29176  usgrnloop0ALT  29237  uhgrnbgr0nb  29386  nbgr0edg  29389  vtxd0nedgb  29521  vtxdusgr0edgnelALT  29529  1hevtxdg0  29538  usgrvd0nedg  29566  uhgrvd00  29567  pthdlem2lem  29800  nmounbi  30805  lnon0  30827  largei  32296  cvbr2  32312  chrelat2i  32394  n0nsnel  32543  uniinn0  32571  infxrge0gelb  32777  nn0min  32827  toslublem  32947  tosglblem  32949  archiabl  33188  lmdvg  33914  esumcvgre  34072  eulerpartlems  34342  bnj110  34851  bnj1417  35034  lfuhgr3  35104  fmlaomn0  35375  fmla0disjsuc  35383  fmlasucdisj  35384  dfon2lem8  35772  dfint3  35934  relowlpssretop  37347  domalom  37387  fvineqsneq  37395  poimirlem26  37633  poimirlem30  37637  poimir  37640  mblfinlem1  37644  ftc1anc  37688  heiborlem1  37798  lcvbr2  39004  lcvbr3  39005  cvrnbtwn  39253  cvrval2  39256  hlrelat2  39386  cdleme0nex  40273  aks4d1p7  42065  sticksstones1  42128  infdesc  42630  nna4b4nsq  42647  rencldnfilem  42808  setindtr  43013  onmaxnelsup  43212  onsupnmax  43217  onsupmaxb  43228  onsupeqnmax  43236  ordnexbtwnsuc  43257  gneispace  44124  nelrnmpt  45024  iindif2f  45103  ralfal  45104  supxrgere  45283  supxrgelem  45287  infxrbnd2  45319  supminfxr  45414  limsupub  45660  limsuppnflem  45666  limsupre2lem  45680  stirlinglem5  46034  etransclem24  46214  etransclem32  46222  sge0iunmpt  46374  sge0rpcpnf  46377  iundjiun  46416  voliunsge0lem  46428  meaiuninc3v  46440  meaiininclem  46442  hoidmv1lelem3  46549  hoidmvlelem4  46554  hoidmvlelem5  46555  n0nsn2el  46975  0nelsetpreimafv  47315  stgr0  47863  gpg5nbgrvtx03starlem1  47959  gpg5nbgrvtx03starlem2  47960  gpg5nbgrvtx03starlem3  47961  gpg5nbgrvtx13starlem1  47962  gpg5nbgrvtx13starlem2  47963  gpg5nbgrvtx13starlem3  47964  copisnmnd  48013  lindslinindsimp1  48303  lindslinindsimp2  48309  ldepslinc  48355  aacllem  49032