Theorem 19.21v 1287

Description: Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as (ph -> A.xph) in 19.21 1058 via the use of distinct variable conditions combined with ax-17 973. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 1386 derived from df-eu 1384. The "f" stands for "not free in" which is less restrictive than "does not occur in."

Assertion

Ref	Expression
19.21v	|- (A.x(ph -> ps) <-> (ph -> A.xps))

Distinct variable group:   ph,x

Proof of Theorem 19.21v

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 |- (ph -> A.xph)
2	1	19.21 1058	1 |- (A.x(ph -> ps) <-> (ph -> A.xps))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 956

This theorem is referenced by:  19.12vv 1304  cbvald 1322  sbcom2 1336  2sb6 1338  2sb6rf 1341  2exsb 1353  r2al 1679  r3al 1693  reu2 1933  unissb 2533  dfiin2 2593  iunss 2596  ssiin 2604  axrep5 2704  asymref 3446  asymref2 3447  f1fv 3881  aceq1 4746  kmlem15 4796

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain