Theorem exiisub-P5 655

Description: Existential Quantifier Introduction Law with Implicit Substitution.

'𝑥' cannot occur in either '𝑡' or '𝜓'.

This is the dual of specisub-P5 654.

The hypothesis is fulfilled when every free occurence of '𝑥' in '𝜑' is replaced with the term '𝑡', and every bound occurence of '𝑥' is replaced with a fresh variable (one for each quantifier). The resulting WFF is '𝜓'. '𝑥' cannot occur in '𝑡' either, or it would occur in '𝜓' wherever '𝑥' was replaced.

Hypothesis

Ref	Expression
exiisub-P5.1	⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
exiisub-P5	⊢ (𝜓 → ∃𝑥𝜑)

Distinct variable groups:   𝜓,𝑥   𝑡,𝑥

Proof of Theorem exiisub-P5

Step	Hyp	Ref	Expression
1		exiisub-P5.1	. . . . 5 ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))
2	1	subneg-P3.39 323	. . . 4 ⊢ (𝑥 = 𝑡 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	specisub-P5 654	. . 3 ⊢ (∀𝑥 ¬ 𝜑 → ¬ 𝜓)
4		allnegex-P5 597	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
5	3, 4	subiml2-P4.RC 541	. 2 ⊢ (¬ ∃𝑥𝜑 → ¬ 𝜓)
6	5	trnsp-P3.31d.RC 289	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8  ¬ wff-neg 9   → wff-imp 10   ↔ wff-bi 104  ∃wff-exists 595

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596

This theorem is referenced by:  qremexv-P5  657