Theorem psubneg-P6-L1 787

Description: Lemma for psubneg-P6 788.

Assertion

Ref	Expression
psubneg-P6-L1	⊢ (∀𝑥(𝑥 = 𝑡 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑡 ∧ 𝜑))

Proof of Theorem psubneg-P6-L1

Step	Hyp	Ref	Expression
1		allasex-P5 599	. 2 ⊢ (∀𝑥(𝑥 = 𝑡 → ¬ 𝜑) ↔ ¬ ∃𝑥 ¬ (𝑥 = 𝑡 → ¬ 𝜑))
2		andasim-P3.46a 356	. . . . 5 ⊢ ((𝑥 = 𝑡 ∧ 𝜑) ↔ ¬ (𝑥 = 𝑡 → ¬ 𝜑))
3	2	bisym-P3.33b.RC 299	. . . 4 ⊢ (¬ (𝑥 = 𝑡 → ¬ 𝜑) ↔ (𝑥 = 𝑡 ∧ 𝜑))
4	3	subexinf-P5 608	. . 3 ⊢ (∃𝑥 ¬ (𝑥 = 𝑡 → ¬ 𝜑) ↔ ∃𝑥(𝑥 = 𝑡 ∧ 𝜑))
5	4	subneg-P3.39.RC 324	. 2 ⊢ (¬ ∃𝑥 ¬ (𝑥 = 𝑡 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑡 ∧ 𝜑))
6	1, 5	bitrns-P3.33c.RC 303	1 ⊢ (∀𝑥(𝑥 = 𝑡 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑡 ∧ 𝜑))

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8  ¬ wff-neg 9   → wff-imp 10   ↔ wff-bi 104   ∧ wff-and 132  ∃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

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:  psubneg-P6  788