Theorem 19.21v 1280

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

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

This theorem is referenced by:  19.12vv 1297  cbvald 1315  sbcom2 1329  2sb6 1331  2sb6rf 1334  2exsb 1346  r2al 1668  r3al 1682  reu2 1920  unissb 2518  dfiin2 2578  iunss 2581  ssiin 2589  axrep5 2688  asymref 3423  asymref2 3424  asymrefOLD 3425  asymref2OLD 3426  f1fv 3859  aceq1 4701  kmlem15 4751

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain