bnj984

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj984.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj984.11	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
Assertion	bnj984	⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj984.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
2		bnj984.11	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
3	2	eleq2i	⊢ ( 𝐺 ∈ 𝐵 ↔ 𝐺 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } )
4		sbc8g	⊢ ( 𝐺 ∈ 𝐴 → ( [ 𝐺 / 𝑓 ] ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ 𝐺 ∈ { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) } ) )
5	3 4	bitr4id	⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
6		df-rex	⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
7		bnj252	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
8	1 7	bitri	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
9	6 8	bnj133	⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑛 𝜒 )
10	9	sbcbii	⊢ ( [ 𝐺 / 𝑓 ] ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 )
11	5 10	bitrdi	⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ 𝐵 ↔ [ 𝐺 / 𝑓 ] ∃ 𝑛 𝜒 ) )

Metamath Proof Explorer

Theorem bnj984

Proof