Theorem 2ralunsn 3560

Description: Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)

Hypotheses

Ref	Expression
2ralunsn.1	|- (x = B -> (ph <-> ch))
2ralunsn.2	|- (y = B -> (ph <-> ps))
2ralunsn.3	|- (x = B -> (ps <-> th))

Assertion

Ref	Expression
2ralunsn	|- (B e. C -> (A.x e. (A u. {B })A.y e. (A u. {B })ph <-> ((A.x e. A A.y e. A ph /\ A.x e. A ps) /\ (A.y e. A ch /\ th))))

Distinct variable groups:   x,A   x,B,y   x, C   ch,x   ps,y   th,x

Allowed substitution hints:   ph(x,y)   ps(x)   ch(y)   th(y)   A(y)   C(y)

Proof of Theorem 2ralunsn

Step	Hyp	Ref	Expression
1		2ralunsn.2	. . . 4 |- (y = B -> (ph <-> ps))
2	1	ralunsn 3559	. . 3 |- (B e. C -> (A.y e. (A u. {B })ph <-> (A.y e. A ph /\ ps)))
3	2	ralbidv 2320	. 2 |- (B e. C -> (A.x e. (A u. {B })A.y e. (A u. {B })ph <-> A.x e. (A u. {B })(A.y e. A ph /\ ps)))
4		2ralunsn.1	. . . . . 6 |- (x = B -> (ph <-> ch))
5	4	ralbidv 2320	. . . . 5 |- (x = B -> (A.y e. A ph <-> A.y e. A ch))
6		2ralunsn.3	. . . . 5 |- (x = B -> (ps <-> th))
7	5, 6	anbi12d 442	. . . 4 |- (x = B -> ((A.y e. A ph /\ ps) <-> (A.y e. A ch /\ th)))
8	7	ralunsn 3559	. . 3 |- (B e. C -> (A.x e. (A u. {B })(A.y e. A ph /\ ps) <-> (A.x e. A (A.y e. A ph /\ ps) /\ (A.y e. A ch /\ th))))
9		r19.26 2435	. . . 4 |- (A.x e. A (A.y e. A ph /\ ps) <-> (A.x e. A A.y e. A ph /\ A.x e. A ps))
10	9	anbi1i 431	. . 3 |- ((A.x e. A (A.y e. A ph /\ ps) /\ (A.y e. A ch /\ th)) <-> ((A.x e. A A.y e. A ph /\ A.x e. A ps) /\ (A.y e. A ch /\ th)))
11	8, 10	syl6bb 185	. 2 |- (B e. C -> (A.x e. (A u. {B })(A.y e. A ph /\ ps) <-> ((A.x e. A A.y e. A ph /\ A.x e. A ps) /\ (A.y e. A ch /\ th))))
12	3, 11	bitrd 177	1 |- (B e. C -> (A.x e. (A u. {B })A.y e. (A u. {B })ph <-> ((A.x e. A A.y e. A ph /\ A.x e. A ps) /\ (A.y e. A ch /\ th))))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   = wceq 1242   e. wcel 1390  A.wral 2300   u. cun 2909   {csn 3367

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-v 2553  df-sbc 2759  df-un 2916  df-sn 3373

This theorem is referenced by: (None)