Theorem cbvexv-P5 660

Description: Change of Bound Variable Law for '∃𝑥' (variable restriction).

'𝑥' cannot occur in '𝜓' and '𝑦' cannot occur in '𝜑'.

The hypothesis is fulfilled when every free occurrence of '𝑥' in '𝜑' is replaced with '𝑦', and every bound occurance of '𝑥' is replaced with a fresh variable (one for each quantifier). The resulting WFF is '𝜓'.

The most general form is cbvex-P6 752.

Hypothesis

Ref	Expression
cbvexv-P5.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvexv-P5	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦

Proof of Theorem cbvexv-P5

Step	Hyp	Ref	Expression
1		df-exists-D5.1 596	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
2		cbvexv-P5.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	subneg-P3.39 323	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
4	3	cbvallv-P5 659	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
5	4	subneg-P3.39.RC 324	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
6		df-exists-D5.1 596	. . 3 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	6	bisym-P3.33b.RC 299	. 2 ⊢ (¬ ∀𝑦 ¬ 𝜓 ↔ ∃𝑦𝜓)
8	1, 5, 7	dbitrns-P4.16.RC 429	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:  genexw-P6  677  nfrex1w-P6  693  example-E6.02a  712