Theorem exiw-P5 662

Description: Weak Version of Existential Quantifier Introduction Law.

This is the dual form of specw-P5 661.

Note that the hypothesis only requires the existence of a dummy variable '𝑥₁' and dummy formula '𝜑₁', that is equivalent to '𝜑' with free occurences of '𝑥' replaced with '𝑥₁' and bound occurances of '𝑥' replaced with fresh variables.

We will need the auxiliary "scheme completeness" axiom ax-L12 29 to eliminate the hypothesis in the general case (see exi-P6 718).

Hypothesis

Ref	Expression
exiw-P5.1	⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))

Assertion

Ref	Expression
exiw-P5	⊢ (𝜑 → ∃𝑥𝜑)

Distinct variable groups:   𝜑,𝑥₁   𝜑₁,𝑥   𝑥,𝑥₁

Proof of Theorem exiw-P5

Step	Hyp	Ref	Expression
1		exiw-P5.1	. . . . 5 ⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))
2	1	subneg-P3.39 323	. . . 4 ⊢ (𝑥 = 𝑥₁ → (¬ 𝜑 ↔ ¬ 𝜑₁))
3	2	specw-P5 661	. . 3 ⊢ (∀𝑥 ¬ 𝜑 → ¬ 𝜑)
4	3	trnsp-P3.31a.RC 280	. 2 ⊢ (𝜑 → ¬ ∀𝑥 ¬ 𝜑)
5		df-exists-D5.1 596	. . 3 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6	5	bisym-P3.33b.RC 299	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ∃𝑥𝜑)
7	4, 6	subimr2-P4.RC 543	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  ax-L7 19

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:  nfrgenw-P6  684  qremexw-P6  703