Theorem 19.21v 1285

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 1056 via the use of distinct variable conditions combined with ax-17 971. 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 1384 derived from df-eu 1382. 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 971	. 2 |- (ph -> A.xph)
2	1	19.21 1056	1 |- (A.x(ph -> ps) <-> (ph -> A.xps))

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

This theorem is referenced by:  19.12vv 1302  cbvald 1320  sbcom2 1334  2sb6 1336  2sb6rf 1339  2exsb 1351  r2al 1676  r3al 1690  reu2 1930  unissb 2528  dfiin2 2588  iunss 2591  ssiin 2599  axrep5 2698  asymref 3439  asymref2 3440  f1fv 3874  aceq1 4729  kmlem15 4779

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain