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

Metamath Proof Explorer

Theorem bnj976

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

Ref Expression
Hypotheses bnj976.1 ⊢ ( 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) )
bnj976.2 ⊢ ( 𝜑′ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
bnj976.3 ⊢ ( 𝜓′ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
bnj976.4 ⊢ ( 𝜒′ ↔ [ 𝐺 / 𝑓 ] 𝜒 )
bnj976.5 ⊢ 𝐺 ∈ V
Assertion bnj976 ( 𝜒′ ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) )

Proof

Step Hyp Ref Expression
1 bnj976.1 ⊢ ( 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) )
2 bnj976.2 ⊢ ( 𝜑′ ↔ [ 𝐺 / 𝑓 ] 𝜑 )
3 bnj976.3 ⊢ ( 𝜓′ ↔ [ 𝐺 / 𝑓 ] 𝜓 )
4 bnj976.4 ⊢ ( 𝜒′ ↔ [ 𝐺 / 𝑓 ] 𝜒 )
5 bnj976.5 ⊢ 𝐺 ∈ V
6 sbccow ⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜒 ↔ [ 𝐺 / 𝑓 ] 𝜒 )
7 bnj252 ⊢ ( ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) )
8 7 sbcbii ⊢ ( [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) )
9 1 sbcbii ⊢ ( [ ℎ / 𝑓 ] 𝜒 ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) )
10 vex ⊢ ℎ ∈ V
11 10 bnj525 ⊢ ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ↔ 𝑁 ∈ 𝐷 )
12 sbc3an ⊢ ( [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) )
13 bnj62 ⊢ ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ↔ ℎ Fn 𝑁 )
14 13 3anbi1i ⊢ ( ( [ ℎ / 𝑓 ] 𝑓 Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) )
15 12 14 bitri ⊢ ( [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ↔ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) )
16 11 15 anbi12i ⊢ ( ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ∧ [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) )
17 sbcan ⊢ ( [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( [ ℎ / 𝑓 ] 𝑁 ∈ 𝐷 ∧ [ ℎ / 𝑓 ] ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) )
18 bnj252 ⊢ ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) )
19 16 17 18 3bitr4ri ⊢ ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ [ ℎ / 𝑓 ] ( 𝑁 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑁 ∧ 𝜑 ∧ 𝜓 ) ) )
20 8 9 19 3bitr4i ⊢ ( [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) )
21 fneq1 ⊢ ( ℎ = 𝐺 → ( ℎ Fn 𝑁 ↔ 𝐺 Fn 𝑁 ) )
22 sbceq1a ⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜑 ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 ) )
23 sbccow ⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 ↔ [ 𝐺 / 𝑓 ] 𝜑 )
24 2 23 bitr4i ⊢ ( 𝜑′ ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜑 )
25 22 24 bitr4di ⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜑 ↔ 𝜑′ ) )
26 sbceq1a ⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜓 ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 ) )
27 sbccow ⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 ↔ [ 𝐺 / 𝑓 ] 𝜓 )
28 3 27 bitr4i ⊢ ( 𝜓′ ↔ [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜓 )
29 26 28 bitr4di ⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜓 ↔ 𝜓′ ) )
30 21 25 29 3anbi123d ⊢ ( ℎ = 𝐺 → ( ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) )
31 30 anbi2d ⊢ ( ℎ = 𝐺 → ( ( 𝑁 ∈ 𝐷 ∧ ( ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) ) )
32 bnj252 ⊢ ( ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( 𝑁 ∈ 𝐷 ∧ ( 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) )
33 31 18 32 3bitr4g ⊢ ( ℎ = 𝐺 → ( ( 𝑁 ∈ 𝐷 ∧ ℎ Fn 𝑁 ∧ [ ℎ / 𝑓 ] 𝜑 ∧ [ ℎ / 𝑓 ] 𝜓 ) ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) )
34 20 33 bitrid ⊢ ( ℎ = 𝐺 → ( [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) ) )
35 5 34 sbcie ⊢ ( [ 𝐺 / ℎ ] [ ℎ / 𝑓 ] 𝜒 ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) )
36 4 6 35 3bitr2i ⊢ ( 𝜒′ ↔ ( 𝑁 ∈ 𝐷 ∧ 𝐺 Fn 𝑁 ∧ 𝜑′ ∧ 𝜓′ ) )