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 syl5bb ( = 𝐺 → ( [ / 𝑓 ] 𝜒 ↔ ( 𝑁𝐷𝐺 Fn 𝑁𝜑′𝜓′ ) ) )
35 5 34 sbcie ( [ 𝐺 / ] [ / 𝑓 ] 𝜒 ↔ ( 𝑁𝐷𝐺 Fn 𝑁𝜑′𝜓′ ) )
36 4 6 35 3bitr2i ( 𝜒′ ↔ ( 𝑁𝐷𝐺 Fn 𝑁𝜑′𝜓′ ) )