Theorem ralnex 1209

Description: Relationship between restricted universal and existential quantifiers.

Assertion

Ref	Expression
ralnex	|- (A.x e. A -. ph <-> -. E.x e. A ph)

Proof of Theorem ralnex

Step	Hyp	Ref	Expression
1		alinexa 724	. 2 |- (A.x(x e. A -> -. ph) <-> -. E.x(x e. A /\ ph))
2		df-ral 1205	. 2 |- (A.x e. A -. ph <-> A.x(x e. A -> -. ph))
3		df-rex 1206	. . 3 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
4	3	negbii 162	. 2 |- (-. E.x e. A ph <-> -. E.x(x e. A /\ ph))
5	1, 2, 4	3bitr4 158	1 |- (A.x e. A -. ph <-> -. E.x e. A ph)

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672  E.wex 678   e. wcel 1092  A.wral 1201  E.wrex 1202

This theorem is referenced by:  dfrex2 1212  nrex 1270  nrexdv 1271  iindif2 2033  supmo 2156  tfi 2244  canth 2945  omsdomnn 3424  isfinite2 3437  eirrv 3449  unbndrank 3527  kmlem7 3586  kmlem12 3591  kmlem13 3592  arch 4521  indstr 4611  sqr2irrlem3 4779  climunii 4883  hlimunii 5143  large 5700  cvbr2t 5715  chrelat2 5758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-ral 1205  df-rex 1206

metamath.org