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  27322  cuteq1  27335  tglowdim2ln  27933  axcontlem12  28264  umgrnloop0  28400  numedglnl  28435  usgrnloop0ALT  28493  uhgrnbgr0nb  28642  nbgr0edg  28645  vtxd0nedgb  28776  vtxdusgr0edgnelALT  28784  1hevtxdg0  28793  usgrvd0nedg  28821  uhgrvd00  28822  pthdlem2lem  29055  nmounbi  30060  lnon0  30082  largei  31551  cvbr2  31567  chrelat2i  31649  uniinn0  31813  infxrge0gelb  32010  nn0min  32057  toslublem  32173  tosglblem  32175  archiabl  32375  lmdvg  32964  esumcvgre  33120  eulerpartlems  33390  bnj110  33900  bnj1417  34083  lfuhgr3  34141  fmlaomn0  34412  fmla0disjsuc  34420  fmlasucdisj  34421  dfon2lem8  34793  dfint3  34955  relowlpssretop  36293  domalom  36333  fvineqsneq  36341  poimirlem26  36562  poimirlem30  36566  poimir  36569  mblfinlem1  36573  ftc1anc  36617  heiborlem1  36727  lcvbr2  37940  lcvbr3  37941  cvrnbtwn  38189  cvrval2  38192  hlrelat2  38322  cdleme0nex  39209  aks4d1p7  40996  sticksstones1  41010  infdesc  41433  nna4b4nsq  41450  rencldnfilem  41606  setindtr  41811  onmaxnelsup  42020  onsupnmax  42025  onsupmaxb  42036  onsupeqnmax  42044  ordnexbtwnsuc  42065  gneispace  42933  nelrnmpt  43821  iindif2f  43902  ralfal  43903  supxrgere  44091  supxrgelem  44095  infxrbnd2  44127  supminfxr  44222  limsupub  44468  limsuppnflem  44474  limsupre2lem  44488  stirlinglem5  44842  etransclem24  45022  etransclem32  45030  sge0iunmpt  45182  sge0rpcpnf  45185  iundjiun  45224  voliunsge0lem  45236  meaiuninc3v  45248  meaiininclem  45250  hoidmv1lelem3  45357  hoidmvlelem4  45362  hoidmvlelem5  45363  n0nsn2el  45783  0nelsetpreimafv  46106  copisnmnd  46627  lindslinindsimp1  47186  lindslinindsimp2  47192  ldepslinc  47238  aacllem  47896