# Metamath Proof Explorer

## Theorem crefdf

Description: A formulation of crefi easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020)

Ref Expression
Hypotheses crefi.x ${⊢}{X}=\bigcup {J}$
crefdf.b ${⊢}{B}=\mathrm{CovHasRef}{A}$
crefdf.p ${⊢}{z}\in {A}\to {\phi }$
Assertion crefdf ${⊢}\left({J}\in {B}\wedge {C}\subseteq {J}\wedge {X}=\bigcup {C}\right)\to \exists {z}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {z}\mathrm{Ref}{C}\right)$

### Proof

Step Hyp Ref Expression
1 crefi.x ${⊢}{X}=\bigcup {J}$
2 crefdf.b ${⊢}{B}=\mathrm{CovHasRef}{A}$
3 crefdf.p ${⊢}{z}\in {A}\to {\phi }$
4 2 eleq2i ${⊢}{J}\in {B}↔{J}\in \mathrm{CovHasRef}{A}$
5 1 crefi ${⊢}\left({J}\in \mathrm{CovHasRef}{A}\wedge {C}\subseteq {J}\wedge {X}=\bigcup {C}\right)\to \exists {z}\in \left(𝒫{J}\cap {A}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{C}$
6 4 5 syl3an1b ${⊢}\left({J}\in {B}\wedge {C}\subseteq {J}\wedge {X}=\bigcup {C}\right)\to \exists {z}\in \left(𝒫{J}\cap {A}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{C}$
7 elin ${⊢}{z}\in \left(𝒫{J}\cap {A}\right)↔\left({z}\in 𝒫{J}\wedge {z}\in {A}\right)$
8 3 anim2i ${⊢}\left({z}\in 𝒫{J}\wedge {z}\in {A}\right)\to \left({z}\in 𝒫{J}\wedge {\phi }\right)$
9 7 8 sylbi ${⊢}{z}\in \left(𝒫{J}\cap {A}\right)\to \left({z}\in 𝒫{J}\wedge {\phi }\right)$
10 9 anim1i ${⊢}\left({z}\in \left(𝒫{J}\cap {A}\right)\wedge {z}\mathrm{Ref}{C}\right)\to \left(\left({z}\in 𝒫{J}\wedge {\phi }\right)\wedge {z}\mathrm{Ref}{C}\right)$
11 anass ${⊢}\left(\left({z}\in 𝒫{J}\wedge {\phi }\right)\wedge {z}\mathrm{Ref}{C}\right)↔\left({z}\in 𝒫{J}\wedge \left({\phi }\wedge {z}\mathrm{Ref}{C}\right)\right)$
12 10 11 sylib ${⊢}\left({z}\in \left(𝒫{J}\cap {A}\right)\wedge {z}\mathrm{Ref}{C}\right)\to \left({z}\in 𝒫{J}\wedge \left({\phi }\wedge {z}\mathrm{Ref}{C}\right)\right)$
13 12 reximi2 ${⊢}\exists {z}\in \left(𝒫{J}\cap {A}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{C}\to \exists {z}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {z}\mathrm{Ref}{C}\right)$
14 6 13 syl ${⊢}\left({J}\in {B}\wedge {C}\subseteq {J}\wedge {X}=\bigcup {C}\right)\to \exists {z}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {z}\mathrm{Ref}{C}\right)$