MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mreexexlemd Structured version   Visualization version   GIF version

Theorem mreexexlemd 16570
Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 16574. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
mreexexlemd.1 (𝜑𝑋𝐽)
mreexexlemd.2 (𝜑𝐹 ⊆ (𝑋𝐻))
mreexexlemd.3 (𝜑𝐺 ⊆ (𝑋𝐻))
mreexexlemd.4 (𝜑𝐹 ⊆ (𝑁‘(𝐺𝐻)))
mreexexlemd.5 (𝜑 → (𝐹𝐻) ∈ 𝐼)
mreexexlemd.6 (𝜑 → (𝐹𝐾𝐺𝐾))
mreexexlemd.7 (𝜑 → ∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)))
Assertion
Ref Expression
mreexexlemd (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))
Distinct variable groups:   𝑗,𝐹   𝑗,𝐺   𝑗,𝐻   𝜑,𝑗   𝑢,𝑡,𝑣,𝑖,𝐼,𝑗   𝑡,𝐾,𝑢,𝑣   𝑡,𝑁,𝑢,𝑣   𝑡,𝑋,𝑢,𝑣
Allowed substitution hints:   𝜑(𝑣,𝑢,𝑡,𝑖)   𝐹(𝑣,𝑢,𝑡,𝑖)   𝐺(𝑣,𝑢,𝑡,𝑖)   𝐻(𝑣,𝑢,𝑡,𝑖)   𝐽(𝑣,𝑢,𝑡,𝑖,𝑗)   𝐾(𝑖,𝑗)   𝑁(𝑖,𝑗)   𝑋(𝑖,𝑗)

Proof of Theorem mreexexlemd
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mreexexlemd.6 . 2 (𝜑 → (𝐹𝐾𝐺𝐾))
2 mreexexlemd.4 . 2 (𝜑𝐹 ⊆ (𝑁‘(𝐺𝐻)))
3 mreexexlemd.5 . 2 (𝜑 → (𝐹𝐻) ∈ 𝐼)
4 mreexexlemd.7 . . . 4 (𝜑 → ∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)))
5 simplr 785 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑢 = 𝑓)
65breq1d 4819 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝐾𝑓𝐾))
7 simpr 477 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑣 = 𝑔)
87breq1d 4819 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝐾𝑔𝐾))
96, 8orbi12d 942 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝐾𝑣𝐾) ↔ (𝑓𝐾𝑔𝐾)))
10 simpll 783 . . . . . . . . . . . 12 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑡 = )
117, 10uneq12d 3930 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝑡) = (𝑔))
1211fveq2d 6379 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑁‘(𝑣𝑡)) = (𝑁‘(𝑔)))
135, 12sseq12d 3794 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢 ⊆ (𝑁‘(𝑣𝑡)) ↔ 𝑓 ⊆ (𝑁‘(𝑔))))
145, 10uneq12d 3930 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝑡) = (𝑓))
1514eleq1d 2829 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝑡) ∈ 𝐼 ↔ (𝑓) ∈ 𝐼))
169, 13, 153anbi123d 1560 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) ↔ ((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
17 simpllr 793 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑢 = 𝑓)
18 simpr 477 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
1917, 18breq12d 4822 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑢𝑖𝑓𝑗))
20 simplll 791 . . . . . . . . . . . 12 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑡 = )
2118, 20uneq12d 3930 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑖𝑡) = (𝑗))
2221eleq1d 2829 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑖𝑡) ∈ 𝐼 ↔ (𝑗) ∈ 𝐼))
2319, 22anbi12d 624 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ (𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
24 simplr 785 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑣 = 𝑔)
2524pweqd 4320 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝒫 𝑣 = 𝒫 𝑔)
2623, 25cbvrexdva2 3324 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
2716, 26imbi12d 335 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
28 simpl 474 . . . . . . . . . 10 ((𝑡 = 𝑢 = 𝑓) → 𝑡 = )
2928difeq2d 3890 . . . . . . . . 9 ((𝑡 = 𝑢 = 𝑓) → (𝑋𝑡) = (𝑋))
3029pweqd 4320 . . . . . . . 8 ((𝑡 = 𝑢 = 𝑓) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3130adantr 472 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3227, 31cbvraldva2 3323 . . . . . 6 ((𝑡 = 𝑢 = 𝑓) → (∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3332, 30cbvraldva2 3323 . . . . 5 (𝑡 = → (∀𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3433cbvalvw 2136 . . . 4 (∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
354, 34sylib 209 . . 3 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
36 ssun2 3939 . . . . . 6 𝐻 ⊆ (𝐹𝐻)
3736a1i 11 . . . . 5 (𝜑𝐻 ⊆ (𝐹𝐻))
383, 37ssexd 4966 . . . 4 (𝜑𝐻 ∈ V)
39 mreexexlemd.1 . . . . . . . . 9 (𝜑𝑋𝐽)
40 difexg 4969 . . . . . . . . 9 (𝑋𝐽 → (𝑋𝐻) ∈ V)
4139, 40syl 17 . . . . . . . 8 (𝜑 → (𝑋𝐻) ∈ V)
42 mreexexlemd.2 . . . . . . . 8 (𝜑𝐹 ⊆ (𝑋𝐻))
4341, 42sselpwd 4968 . . . . . . 7 (𝜑𝐹 ∈ 𝒫 (𝑋𝐻))
4443adantr 472 . . . . . 6 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋𝐻))
45 simpr 477 . . . . . . . 8 ((𝜑 = 𝐻) → = 𝐻)
4645difeq2d 3890 . . . . . . 7 ((𝜑 = 𝐻) → (𝑋) = (𝑋𝐻))
4746pweqd 4320 . . . . . 6 ((𝜑 = 𝐻) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
4844, 47eleqtrrd 2847 . . . . 5 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋))
49 mreexexlemd.3 . . . . . . . . 9 (𝜑𝐺 ⊆ (𝑋𝐻))
5041, 49sselpwd 4968 . . . . . . . 8 (𝜑𝐺 ∈ 𝒫 (𝑋𝐻))
5150ad2antrr 717 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋𝐻))
5247adantr 472 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
5351, 52eleqtrrd 2847 . . . . . 6 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋))
54 simplr 785 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
5554breq1d 4819 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝐾𝐹𝐾))
56 simpr 477 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
5756breq1d 4819 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔𝐾𝐺𝐾))
5855, 57orbi12d 942 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝐾𝑔𝐾) ↔ (𝐹𝐾𝐺𝐾)))
59 simpllr 793 . . . . . . . . . . 11 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → = 𝐻)
6056, 59uneq12d 3930 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔) = (𝐺𝐻))
6160fveq2d 6379 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑁‘(𝑔)) = (𝑁‘(𝐺𝐻)))
6254, 61sseq12d 3794 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ⊆ (𝑁‘(𝑔)) ↔ 𝐹 ⊆ (𝑁‘(𝐺𝐻))))
6354, 59uneq12d 3930 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓) = (𝐹𝐻))
6463eleq1d 2829 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓) ∈ 𝐼 ↔ (𝐹𝐻) ∈ 𝐼))
6558, 62, 643anbi123d 1560 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼)))
6656pweqd 4320 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝒫 𝑔 = 𝒫 𝐺)
6754breq1d 4819 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝑗𝐹𝑗))
6859uneq2d 3929 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑗) = (𝑗𝐻))
6968eleq1d 2829 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑗) ∈ 𝐼 ↔ (𝑗𝐻) ∈ 𝐼))
7067, 69anbi12d 624 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ (𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7166, 70rexeqbidv 3301 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7265, 71imbi12d 335 . . . . . 6 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) ↔ (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7353, 72rspcdv 3464 . . . . 5 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7448, 73rspcimdv 3462 . . . 4 ((𝜑 = 𝐻) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7538, 74spcimdv 3442 . . 3 (𝜑 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7635, 75mpd 15 . 2 (𝜑 → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
771, 2, 3, 76mp3and 1588 1 (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wo 873  w3a 1107  wal 1650   = wceq 1652  wcel 2155  wral 3055  wrex 3056  Vcvv 3350  cdif 3729  cun 3730  wss 3732  𝒫 cpw 4315   class class class wbr 4809  cfv 6068  cen 8157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076
This theorem is referenced by:  mreexexlem4d  16573  mreexexd  16574
  Copyright terms: Public domain W3C validator