Theorem 19.21v 1327

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

Syntax hints:   -> wi 3   <-> wb 153  A.wal 995

This theorem is referenced by:  19.12vv 1344  cbvald 1362  sbcom2 1376  2sb6 1378  2sb6rf 1381  2exsb 1393  r2al 1723  r3al 1737  reu2 1977  unissb 2582  dfiin2 2642  iunss 2645  ssiin 2653  axrep5 2753  asymref 3496  asymref2 3497  f1fv 3931  aceq1 4791  kmlem15 4841

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019

This theorem depends on definitions:  df-bi 154

Copyright terms: Public domain