Metamath Proof Explorer

Theorem bnj919

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

Ref Expression
Hypotheses bnj919.1 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
bnj919.2 ⊢ ( 𝜑′ ↔ [ 𝑃 / 𝑛 ] 𝜑 )
bnj919.3 ⊢ ( 𝜓′ ↔ [ 𝑃 / 𝑛 ] 𝜓 )
bnj919.4 ⊢ ( 𝜒′ ↔ [ 𝑃 / 𝑛 ] 𝜒 )
bnj919.5 ⊢ 𝑃 ∈ V
Assertion bnj919 ( 𝜒′ ↔ ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) )

Proof

Step Hyp Ref Expression
1 bnj919.1 ⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
2 bnj919.2 ⊢ ( 𝜑′ ↔ [ 𝑃 / 𝑛 ] 𝜑 )
3 bnj919.3 ⊢ ( 𝜓′ ↔ [ 𝑃 / 𝑛 ] 𝜓 )
4 bnj919.4 ⊢ ( 𝜒′ ↔ [ 𝑃 / 𝑛 ] 𝜒 )
5 bnj919.5 ⊢ 𝑃 ∈ V
6 1 sbcbii ⊢ ( [ 𝑃 / 𝑛 ] 𝜒 ↔ [ 𝑃 / 𝑛 ] ( 𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
7 df-bnj17 ⊢ ( ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ) ∧ 𝜓′ ) )
8 nfv ⊢ Ⅎ 𝑛 𝑃 ∈ 𝐷
9 nfv ⊢ Ⅎ 𝑛 𝐹 Fn 𝑃
10 nfsbc1v ⊢ Ⅎ 𝑛 [ 𝑃 / 𝑛 ] 𝜑
11 2 10 nfxfr ⊢ Ⅎ 𝑛 𝜑′
12 8 9 11 nf3an ⊢ Ⅎ 𝑛 ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ )
13 nfsbc1v ⊢ Ⅎ 𝑛 [ 𝑃 / 𝑛 ] 𝜓
14 3 13 nfxfr ⊢ Ⅎ 𝑛 𝜓′
15 12 14 nfan ⊢ Ⅎ 𝑛 ( ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ) ∧ 𝜓′ )
16 7 15 nfxfr ⊢ Ⅎ 𝑛 ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ )
17 eleq1 ⊢ ( 𝑛 = 𝑃 → ( 𝑛 ∈ 𝐷 ↔ 𝑃 ∈ 𝐷 ) )
18 fneq2 ⊢ ( 𝑛 = 𝑃 → ( 𝐹 Fn 𝑛 ↔ 𝐹 Fn 𝑃 ) )
19 sbceq1a ⊢ ( 𝑛 = 𝑃 → ( 𝜑 ↔ [ 𝑃 / 𝑛 ] 𝜑 ) )
20 19 2 bitr4di ⊢ ( 𝑛 = 𝑃 → ( 𝜑 ↔ 𝜑′ ) )
21 sbceq1a ⊢ ( 𝑛 = 𝑃 → ( 𝜓 ↔ [ 𝑃 / 𝑛 ] 𝜓 ) )
22 21 3 bitr4di ⊢ ( 𝑛 = 𝑃 → ( 𝜓 ↔ 𝜓′ ) )
23 18 20 22 3anbi123d ⊢ ( 𝑛 = 𝑃 → ( ( 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) ) )
24 17 23 anbi12d ⊢ ( 𝑛 = 𝑃 → ( ( 𝑛 ∈ 𝐷 ∧ ( 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ↔ ( 𝑃 ∈ 𝐷 ∧ ( 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) ) ) )
25 bnj252 ⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
26 bnj252 ⊢ ( ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) ↔ ( 𝑃 ∈ 𝐷 ∧ ( 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) ) )
27 24 25 26 3bitr4g ⊢ ( 𝑛 = 𝑃 → ( ( 𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) ) )
28 16 27 sbciegf ⊢ ( 𝑃 ∈ V → ( [ 𝑃 / 𝑛 ] ( 𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) ) )
29 5 28 ax-mp ⊢ ( [ 𝑃 / 𝑛 ] ( 𝑛 ∈ 𝐷 ∧ 𝐹 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) )
30 4 6 29 3bitri ⊢ ( 𝜒′ ↔ ( 𝑃 ∈ 𝐷 ∧ 𝐹 Fn 𝑃 ∧ 𝜑′ ∧ 𝜓′ ) )