Metamath Proof Explorer

Theorem 2uasbanh

Description: Distribute the unabbreviated form of proper substitution in and out of a conjunction. 2uasbanh is derived from 2uasbanhVD . (Contributed by Alan Sare, 31-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis 2uasbanh.1 ⊢ ( 𝜒 ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
Assertion 2uasbanh ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 2uasbanh.1 ⊢ ( 𝜒 ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
2 simpl ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
3 simprl ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝜑 )
4 2 3 jca ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
5 4 2eximi ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
6 simprr ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → 𝜓 )
7 2 6 jca ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
8 7 2eximi ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
9 5 8 jca ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
10 1 simplbi ⊢ ( 𝜒 → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
11 simpl ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
12 11 2eximi ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
13 10 12 syl ⊢ ( 𝜒 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
14 ax6e2ndeq ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
15 13 14 sylibr ⊢ ( 𝜒 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
16 2sb5nd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
17 15 16 syl ⊢ ( 𝜒 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
18 10 17 mpbird ⊢ ( 𝜒 → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
19 1 simprbi ⊢ ( 𝜒 → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
20 2sb5nd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
21 15 20 syl ⊢ ( 𝜒 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
22 19 21 mpbird ⊢ ( 𝜒 → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 )
23 sban ⊢ ( [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑣 / 𝑦 ] 𝜓 ) )
24 23 sbbii ⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑢 / 𝑥 ] ( [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑣 / 𝑦 ] 𝜓 ) )
25 sban ⊢ ( [ 𝑢 / 𝑥 ] ( [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑣 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ) )
26 24 25 bitri ⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ) )
27 18 22 26 sylanbrc ⊢ ( 𝜒 → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) )
28 2sb5nd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) )
29 15 28 syl ⊢ ( 𝜒 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) )
30 27 29 mpbid ⊢ ( 𝜒 → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
31 1 30 sylbir ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
32 9 31 impbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )