Theorem elovmporab1w

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. Version of elovmporab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

	Ref	Expression
Hypotheses	elovmporab1w.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
	elovmporab1w.v	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
Assertion	elovmporab1w	⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		elovmporab1w.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
2		elovmporab1w.v	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
3	1	elmpocl	⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
4	1	a1i	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑧 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } ) )
5		csbeq1	⊢ ( 𝑥 = 𝑋 → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
6	5	ad2antrl	⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
7		sbceq1a	⊢ ( 𝑦 = 𝑌 → ( 𝜑 ↔ [ 𝑌 / 𝑦 ] 𝜑 ) )
8		sbceq1a	⊢ ( 𝑥 = 𝑋 → ( [ 𝑌 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
9	7 8	sylan9bbr	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
10	9	adantl	⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
11	6 10	rabeqbidv	⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑧 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } = { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
12		eqidd	⊢ ( ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑥 = 𝑋 ) → V = V )
13		simpl	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑋 ∈ V )
14		simpr	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑌 ∈ V )
15		rabexg	⊢ ( ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V → { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
16	2 15	syl	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ∈ V )
17		nfcv	⊢ Ⅎ 𝑥 𝑋
18	17	nfel1	⊢ Ⅎ 𝑥 𝑋 ∈ V
19		nfcv	⊢ Ⅎ 𝑥 𝑌
20	19	nfel1	⊢ Ⅎ 𝑥 𝑌 ∈ V
21	18 20	nfan	⊢ Ⅎ 𝑥 ( 𝑋 ∈ V ∧ 𝑌 ∈ V )
22		nfcv	⊢ Ⅎ 𝑦 𝑋
23	22	nfel1	⊢ Ⅎ 𝑦 𝑋 ∈ V
24		nfcv	⊢ Ⅎ 𝑦 𝑌
25	24	nfel1	⊢ Ⅎ 𝑦 𝑌 ∈ V
26	23 25	nfan	⊢ Ⅎ 𝑦 ( 𝑋 ∈ V ∧ 𝑌 ∈ V )
27		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
28		nfcv	⊢ Ⅎ 𝑥 𝑀
29	17 28	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑚 ⦌ 𝑀
30	27 29	nfrabw	⊢ Ⅎ 𝑥 { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 }
31		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝑌 / 𝑦 ] 𝜑
32	22 31	nfsbcw	⊢ Ⅎ 𝑦 [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑
33		nfcv	⊢ Ⅎ 𝑦 𝑀
34	22 33	nfcsbw	⊢ Ⅎ 𝑦 ⦋ 𝑋 / 𝑚 ⦌ 𝑀
35	32 34	nfrabw	⊢ Ⅎ 𝑦 { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 }
36	4 11 12 13 14 16 21 26 22 19 30 35	ovmpodxf	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 𝑂 𝑌 ) = { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } )
37	36	eleq2d	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) ↔ 𝑍 ∈ { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } ) )
38		df-3an	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ↔ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )
39	38	simplbi2com	⊢ ( 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
40		elrabi	⊢ ( 𝑍 ∈ { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
41	39 40	syl11	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ { 𝑧 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 } → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
42	37 41	sylbid	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
43	3 42	mpcom	⊢ ( 𝑍 ∈ ( 𝑋 𝑂 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )