Theorem nfrleq-P6 687

Description: Effective Non-Freeness is Bound to Logical Equivalence .

Hypothesis

Ref	Expression
nfrleq-P6.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
nfrleq-P6	⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)

Proof of Theorem nfrleq-P6

Step	Hyp	Ref	Expression
1		df-nfree-D6.1 682	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑))
2		nfrleq-P6.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	suballinf-P5 594	. . 3 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)
4	2	subneg-P3.39.RC 324	. . . 4 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
5	4	suballinf-P5 594	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓)
6	3, 5	subord-P3.43c.RC 351	. 2 ⊢ ((∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑) ↔ (∀𝑥𝜓 ∨ ∀𝑥 ¬ 𝜓))
7		df-nfree-D6.1 682	. . 3 ⊢ (Ⅎ𝑥𝜓 ↔ (∀𝑥𝜓 ∨ ∀𝑥 ¬ 𝜓))
8	7	bisym-P3.33b.RC 299	. 2 ⊢ ((∀𝑥𝜓 ∨ ∀𝑥 ¬ 𝜓) ↔ Ⅎ𝑥𝜓)
9	1, 6, 8	dbitrns-P4.16.RC 429	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  nfrbi-P6  691  example-E6.01a  706  example-E6.02a  712  lemma-L6.06a  766  psubsuccv-P6  806  psubaddv-P6  808  psubmultv-P6  810  nfrandd-P6  816  nfrord-P6  817  nfrbid-P6  818  nfrnfr-P6  821