This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )