strfvi - Metamath Proof Explorer

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

Theorem strfvi 17130

Description: Structure slot extractors cannot distinguish between proper classes and ∅, so they can be protected using the identity function. (Contributed by Stefan O'Rear, 21-Mar-2015.)

**Hypotheses**
Ref	Expression
strfvi.e	⊢ 𝐸 = Slot 𝑁
strfvi.x	⊢ 𝑋 = (𝐸‘𝑆)

**Assertion**
Ref	Expression
strfvi	⊢ 𝑋 = (𝐸‘( I ‘𝑆))

**Proof of Theorem strfvi**
Step	Hyp	Ref	Expression
1		strfvi.x	. 2 ⊢ 𝑋 = (𝐸‘𝑆)
2		fvi 6967	. . . . 5 ⊢ (𝑆 ∈ V → ( I ‘𝑆) = 𝑆)
3	2	eqcomd 2737	. . . 4 ⊢ (𝑆 ∈ V → 𝑆 = ( I ‘𝑆))
4	3	fveq2d 6895	. . 3 ⊢ (𝑆 ∈ V → (𝐸‘𝑆) = (𝐸‘( I ‘𝑆)))
5		strfvi.e	. . . . 5 ⊢ 𝐸 = Slot 𝑁
6	5	str0 17129	. . . 4 ⊢ ∅ = (𝐸‘∅)
7		fvprc 6883	. . . 4 ⊢ (¬ 𝑆 ∈ V → (𝐸‘𝑆) = ∅)
8		fvprc 6883	. . . . 5 ⊢ (¬ 𝑆 ∈ V → ( I ‘𝑆) = ∅)
9	8	fveq2d 6895	. . . 4 ⊢ (¬ 𝑆 ∈ V → (𝐸‘( I ‘𝑆)) = (𝐸‘∅))
10	6, 7, 9	3eqtr4a 2797	. . 3 ⊢ (¬ 𝑆 ∈ V → (𝐸‘𝑆) = (𝐸‘( I ‘𝑆)))
11	4, 10	pm2.61i 182	. 2 ⊢ (𝐸‘𝑆) = (𝐸‘( I ‘𝑆))
12	1, 11	eqtri 2759	1 ⊢ 𝑋 = (𝐸‘( I ‘𝑆))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1540 ∈ wcel 2105 Vcvv 3473 ∅c0 4322 I cid 5573 ‘cfv 6543 Slot cslot 17121

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-iota 6495 df-fun 6545 df-fv 6551 df-slot 17122

This theorem is referenced by: rlmscaf 21065 islidl 21070 lidlrsppropd 21093 rspsn 21181 ply1tmcl 22114 ply1scltm 22123 ply1sclf 22127 ply1scl0OLD 22133 ply1scl1OLD 22136 nrgtrg 24527

W3C validator