Metamath Proof Explorer

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 ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ ⦋ x / m⦌ M | φ
elovmporab1w.v ⊢ X ∈ V ∧ Y ∈ V → ⦋ X / m⦌ M ∈ V
Assertion elovmporab1w ⊢ Z ∈ X O Y → X ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ X / m⦌ M

Proof

Step Hyp Ref Expression
1 elovmporab1w.o ⊢ O = x ∈ V , y ∈ V ⟼ z ∈ ⦋ x / m⦌ M | φ
2 elovmporab1w.v ⊢ X ∈ V ∧ Y ∈ V → ⦋ X / m⦌ M ∈ V
3 1 elmpocl ⊢ Z ∈ X O Y → X ∈ V ∧ Y ∈ V
4 1 a1i ⊢ X ∈ V ∧ Y ∈ V → O = x ∈ V , y ∈ V ⟼ z ∈ ⦋ x / m⦌ M | φ
5 csbeq1 ⊢ x = X → ⦋ x / m⦌ M = ⦋ X / m⦌ M
6 5 ad2antrl ⊢ X ∈ V ∧ Y ∈ V ∧ x = X ∧ y = Y → ⦋ x / m⦌ M = ⦋ X / m⦌ M
7 sbceq1a ⊢ y = Y → φ ↔ [˙Y / y]˙ φ
8 sbceq1a ⊢ x = X → [˙Y / y]˙ φ ↔ [˙X / x]˙ [˙Y / y]˙ φ
9 7 8 sylan9bbr ⊢ x = X ∧ y = Y → φ ↔ [˙X / x]˙ [˙Y / y]˙ φ
10 9 adantl ⊢ X ∈ V ∧ Y ∈ V ∧ x = X ∧ y = Y → φ ↔ [˙X / x]˙ [˙Y / y]˙ φ
11 6 10 rabeqbidv ⊢ X ∈ V ∧ Y ∈ V ∧ x = X ∧ y = Y → z ∈ ⦋ x / m⦌ M | φ = z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ
12 eqidd ⊢ X ∈ V ∧ Y ∈ V ∧ x = X → V = V
13 simpl ⊢ X ∈ V ∧ Y ∈ V → X ∈ V
14 simpr ⊢ X ∈ V ∧ Y ∈ V → Y ∈ V
15 rabexg ⊢ ⦋ X / m⦌ M ∈ V → z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ ∈ V
16 2 15 syl ⊢ X ∈ V ∧ Y ∈ V → z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ ∈ V
17 nfcv ⊢ Ⅎ _ x X
18 17 nfel1 ⊢ Ⅎ x X ∈ V
19 nfcv ⊢ Ⅎ _ x Y
20 19 nfel1 ⊢ Ⅎ x Y ∈ V
21 18 20 nfan ⊢ Ⅎ x X ∈ V ∧ Y ∈ V
22 nfcv ⊢ Ⅎ _ y X
23 22 nfel1 ⊢ Ⅎ y X ∈ V
24 nfcv ⊢ Ⅎ _ y Y
25 24 nfel1 ⊢ Ⅎ y Y ∈ V
26 23 25 nfan ⊢ Ⅎ y X ∈ V ∧ Y ∈ V
27 nfsbc1v ⊢ Ⅎ x [˙X / x]˙ [˙Y / y]˙ φ
28 nfcv ⊢ Ⅎ _ x M
29 17 28 nfcsbw ⊢ Ⅎ _ x ⦋ X / m⦌ M
30 27 29 nfrabw ⊢ Ⅎ _ x z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ
31 nfsbc1v ⊢ Ⅎ y [˙Y / y]˙ φ
32 22 31 nfsbcw ⊢ Ⅎ y [˙X / x]˙ [˙Y / y]˙ φ
33 nfcv ⊢ Ⅎ _ y M
34 22 33 nfcsbw ⊢ Ⅎ _ y ⦋ X / m⦌ M
35 32 34 nfrabw ⊢ Ⅎ _ y z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ
36 4 11 12 13 14 16 21 26 22 19 30 35 ovmpodxf ⊢ X ∈ V ∧ Y ∈ V → X O Y = z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ
37 36 eleq2d ⊢ X ∈ V ∧ Y ∈ V → Z ∈ X O Y ↔ Z ∈ z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ
38 df-3an ⊢ X ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ X / m⦌ M ↔ X ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ X / m⦌ M
39 38 simplbi2com ⊢ Z ∈ ⦋ X / m⦌ M → X ∈ V ∧ Y ∈ V → X ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ X / m⦌ M
40 elrabi ⊢ Z ∈ z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ → Z ∈ ⦋ X / m⦌ M
41 39 40 syl11 ⊢ X ∈ V ∧ Y ∈ V → Z ∈ z ∈ ⦋ X / m⦌ M | [˙X / x]˙ [˙Y / y]˙ φ → X ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ X / m⦌ M
42 37 41 sylbid ⊢ X ∈ V ∧ Y ∈ V → Z ∈ X O Y → X ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ X / m⦌ M
43 3 42 mpcom ⊢ Z ∈ X O Y → X ∈ V ∧ Y ∈ V ∧ Z ∈ ⦋ X / m⦌ M