Theorem 19.21v 942

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 738 via the use of distinct variable conditions combined with ax-17 925. 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 1011 derived from df-eu 1009. 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(s):   ph,x

Proof of Theorem 19.21v

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

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672

This theorem is referenced by:  19.12vv 960  cbvald 977  sbcom2 992  r2al 1231  r3al 1240  r19.21v 1260  reu2 1338  zfrep3 1476  unissb 1941  dfiin2 2015  iunss 2017  ssiin 2024  f1fv 2916  aceq1 3552  kmlem15 3594

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-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128

metamath.org