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 1055 via the use of distinct variable conditions combined with ax-17 970. 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 970	. 2 |- (ph -> A.xph)
2	1	19.21 1055	1 |- (A.x(ph -> ps) <-> (ph -> A.xps))

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

This theorem is referenced by:  19.12vv 1302  cbvald 1320  sbcom2 1334  2sb6 1336  2sb6rf 1339  2exsb 1351  r2al 1675  r3al 1689  reu2 1928  unissb 2525  dfiin2 2585  iunss 2588  ssiin 2596  axrep5 2695  asymref 3436  asymref2 3437  f1fv 3871  aceq1 4716  kmlem15 4766

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain