Theorem nfrneg-P6 688

Description: ENF Over Negation.

Assertion

Ref	Expression
nfrneg-P6	⊢ (Ⅎ𝑥 ¬ 𝜑 ↔ Ⅎ𝑥𝜑)

Proof of Theorem nfrneg-P6

Step	Hyp	Ref	Expression
1		df-nfree-D6.1 682	. 2 ⊢ (Ⅎ𝑥 ¬ 𝜑 ↔ (∀𝑥 ¬ 𝜑 ∨ ∀𝑥 ¬ ¬ 𝜑))
2		dnegeq-P4.10 418	. . . 4 ⊢ (¬ ¬ 𝜑 ↔ 𝜑)
3	2	suballinf-P5 594	. . 3 ⊢ (∀𝑥 ¬ ¬ 𝜑 ↔ ∀𝑥𝜑)
4	3	suborr-P3.43b.RC 349	. 2 ⊢ ((∀𝑥 ¬ 𝜑 ∨ ∀𝑥 ¬ ¬ 𝜑) ↔ (∀𝑥 ¬ 𝜑 ∨ ∀𝑥𝜑))
5		orcomm-P3.37 319	. 2 ⊢ ((∀𝑥 ¬ 𝜑 ∨ ∀𝑥𝜑) ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑))
6		df-nfree-D6.1 682	. . 3 ⊢ (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑))
7	6	bisym-P3.33b.RC 299	. 2 ⊢ ((∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑) ↔ Ⅎ𝑥𝜑)
8	1, 4, 5, 7	tbitrns-P4.17.RC 431	1 ⊢ (Ⅎ𝑥 ¬ 𝜑 ↔ Ⅎ𝑥𝜑)

Syntax hints:  ∀wff-forall 8  ¬ wff-neg 9   ↔ wff-bi 104   ∨ wff-or 144  Ⅎwff-nfree 681

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-nfree-D6.1 682

This theorem is referenced by:  nfrand-P6  690  nfrex2w-P6  695  nfrexgenw-P6  696  exgennfrw-P6  697  nfrexgen-P6  735  exgennfr-P6  736  genall-P6  737  cbvex-P6  752  qcexandl-P6  762  nfrexgencl-L6  813  exgennfrcl-L6  814  nfrandd-P6  816  nfrord-P6  817  ndnfrneg-P7.2  827