Metamath Proof Explorer

Theorem eliin2f

Description: Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis eliin2f.1 ⊢Ⅎ_xB
Assertion eliin2f ⊢B≠∅→A∈⋂x∈BC↔∀x∈BA∈C

Proof

Step Hyp Ref Expression
1 eliin2f.1 ⊢Ⅎ_xB
2 eliin ⊢A∈V→A∈⋂x∈BC↔∀x∈BA∈C
3 2 adantl ⊢B≠∅∧A∈V→A∈⋂x∈BC↔∀x∈BA∈C
4 prcnel ⊢¬A∈V→¬A∈⋂x∈BC
5 4 adantl ⊢B≠∅∧¬A∈V→¬A∈⋂x∈BC
6 n0 ⊢B≠∅↔∃yy∈B
7 6 biimpi ⊢B≠∅→∃yy∈B
8 7 adantr ⊢B≠∅∧¬A∈V→∃yy∈B
9 prcnel ⊢¬A∈V→¬A∈⦋y/x⦌C
10 9 a1d ⊢¬A∈V→y∈B→¬A∈⦋y/x⦌C
11 10 adantl ⊢B≠∅∧¬A∈V→y∈B→¬A∈⦋y/x⦌C
12 11 ancld ⊢B≠∅∧¬A∈V→y∈B→y∈B∧¬A∈⦋y/x⦌C
13 12 eximdv ⊢B≠∅∧¬A∈V→∃yy∈B→∃yy∈B∧¬A∈⦋y/x⦌C
14 8 13 mpd ⊢B≠∅∧¬A∈V→∃yy∈B∧¬A∈⦋y/x⦌C
15 df-rex ⊢∃y∈B¬A∈⦋y/x⦌C↔∃yy∈B∧¬A∈⦋y/x⦌C
16 14 15 sylibr ⊢B≠∅∧¬A∈V→∃y∈B¬A∈⦋y/x⦌C
17 nfcv ⊢Ⅎ_yB
18 nfv ⊢Ⅎy¬A∈C
19 nfcsb1v ⊢Ⅎ_x⦋y/x⦌C
20 19 nfel2 ⊢ℲxA∈⦋y/x⦌C
21 20 nfn ⊢Ⅎx¬A∈⦋y/x⦌C
22 csbeq1a ⊢x=y→C=⦋y/x⦌C
23 22 eleq2d ⊢x=y→A∈C↔A∈⦋y/x⦌C
24 23 notbid ⊢x=y→¬A∈C↔¬A∈⦋y/x⦌C
25 1 17 18 21 24 cbvrexfw ⊢∃x∈B¬A∈C↔∃y∈B¬A∈⦋y/x⦌C
26 16 25 sylibr ⊢B≠∅∧¬A∈V→∃x∈B¬A∈C
27 rexnal ⊢∃x∈B¬A∈C↔¬∀x∈BA∈C
28 26 27 sylib ⊢B≠∅∧¬A∈V→¬∀x∈BA∈C
29 5 28 2falsed ⊢B≠∅∧¬A∈V→A∈⋂x∈BC↔∀x∈BA∈C
30 3 29 pm2.61dan ⊢B≠∅→A∈⋂x∈BC↔∀x∈BA∈C