Theorem rexim 2194

Description: Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (The proof was shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
rexim	|- (A.x e. A (ph -> ps) -> (E.x e. A ph -> E.x e. A ps))

Proof of Theorem rexim

Step	Hyp	Ref	Expression
1		con3 110	. . . 4 |- ((ph -> ps) -> (-. ps -> -. ph))
2	1	ral2imi 2169	. . 3 |- (A.x e. A (ph -> ps) -> (A.x e. A -. ps -> A.x e. A -. ph))
3	2	con3d 111	. 2 |- (A.x e. A (ph -> ps) -> (-. A.x e. A -. ph -> -. A.x e. A -. ps))
4		ralnex 2113	. . 3 |- (A.x e. A -. ph <-> -. E.x e. A ph)
5	4	con2bii 238	. 2 |- (E.x e. A ph <-> -. A.x e. A -. ph)
6		ralnex 2113	. . 3 |- (A.x e. A -. ps <-> -. E.x e. A ps)
7	6	con2bii 238	. 2 |- (E.x e. A ps <-> -. A.x e. A -. ps)
8	3, 5, 7	3imtr4g 612	1 |- (A.x e. A (ph -> ps) -> (E.x e. A ph -> E.x e. A ps))

Syntax hints:  -. wn 2   -> wi 3  A.wral 2105  E.wrex 2106

This theorem is referenced by:  reximia 2196  reximdai 2199  r19.29 2227  ss2iun 3271  ficardom 5979  negeui 6510  receui 6890  bnj44 12419  bnj44OLD 12420  bnj48 12422  bnj48OLD 12423  bnj55 12430  dstr 14516

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain