Theorem bnj156

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj156.1	⊢ ( 𝜁0 ↔ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
	bnj156.2	⊢ ( 𝜁1 ↔ [ 𝑔 / 𝑓 ] 𝜁0 )
	bnj156.3	⊢ ( 𝜑1 ↔ [ 𝑔 / 𝑓 ] 𝜑′ )
	bnj156.4	⊢ ( 𝜓1 ↔ [ 𝑔 / 𝑓 ] 𝜓′ )
Assertion	bnj156	⊢ ( 𝜁1 ↔ ( 𝑔 Fn 1o ∧ 𝜑1 ∧ 𝜓1 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj156.1	⊢ ( 𝜁0 ↔ ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
2		bnj156.2	⊢ ( 𝜁1 ↔ [ 𝑔 / 𝑓 ] 𝜁0 )
3		bnj156.3	⊢ ( 𝜑1 ↔ [ 𝑔 / 𝑓 ] 𝜑′ )
4		bnj156.4	⊢ ( 𝜓1 ↔ [ 𝑔 / 𝑓 ] 𝜓′ )
5	1	sbcbii	⊢ ( [ 𝑔 / 𝑓 ] 𝜁0 ↔ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) )
6		sbc3an	⊢ ( [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( [ 𝑔 / 𝑓 ] 𝑓 Fn 1o ∧ [ 𝑔 / 𝑓 ] 𝜑′ ∧ [ 𝑔 / 𝑓 ] 𝜓′ ) )
7		bnj62	⊢ ( [ 𝑔 / 𝑓 ] 𝑓 Fn 1o ↔ 𝑔 Fn 1o )
8	3	bicomi	⊢ ( [ 𝑔 / 𝑓 ] 𝜑′ ↔ 𝜑1 )
9	4	bicomi	⊢ ( [ 𝑔 / 𝑓 ] 𝜓′ ↔ 𝜓1 )
10	7 8 9	3anbi123i	⊢ ( ( [ 𝑔 / 𝑓 ] 𝑓 Fn 1o ∧ [ 𝑔 / 𝑓 ] 𝜑′ ∧ [ 𝑔 / 𝑓 ] 𝜓′ ) ↔ ( 𝑔 Fn 1o ∧ 𝜑1 ∧ 𝜓1 ) )
11	6 10	bitri	⊢ ( [ 𝑔 / 𝑓 ] ( 𝑓 Fn 1o ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( 𝑔 Fn 1o ∧ 𝜑1 ∧ 𝜓1 ) )
12	5 11	bitri	⊢ ( [ 𝑔 / 𝑓 ] 𝜁0 ↔ ( 𝑔 Fn 1o ∧ 𝜑1 ∧ 𝜓1 ) )
13	2 12	bitri	⊢ ( 𝜁1 ↔ ( 𝑔 Fn 1o ∧ 𝜑1 ∧ 𝜓1 ) )