Theorem 2sb5nd

Description: Equivalence for double substitution 2sb5 without distinct x , y requirement. 2sb5nd is derived from 2sb5ndVD . (Contributed by Alan Sare, 30-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	2sb5nd	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax6e2ndeq	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
2		anabs5	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
3		2pm13.193	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
4	3	exbii	⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
5		nfs1v	⊢ Ⅎ 𝑦 [ 𝑣 / 𝑦 ] 𝜑
6	5	nfsb	⊢ Ⅎ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑
7	6	19.41	⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
8	4 7	bitr3i	⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
9	8	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
10		nfs1v	⊢ Ⅎ 𝑥 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑
11	10	19.41	⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
12	9 11	bitr2i	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
13	12	anbi2i	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
14	2 13	bitr3i	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
15		pm5.32	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) ) ↔ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) ) )
16	14 15	mpbir	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
17	1 16	sylbi	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )