ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2rmorex GIF version

Theorem 2rmorex 2739
Description: Double restricted quantification with "at most one," analogous to 2moex 1983. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
Assertion
Ref Expression
2rmorex (∃*x A y B φy B ∃*x A φ)
Distinct variable groups:   y,A   x,B   x,y
Allowed substitution hints:   φ(x,y)   A(x)   B(y)

Proof of Theorem 2rmorex
StepHypRef Expression
1 df-rex 2306 . . . . . . . 8 (y B φy(y B φ))
21anbi2i 430 . . . . . . 7 ((x A y B φ) ↔ (x A y(y B φ)))
32mobii 1934 . . . . . 6 (∃*x(x A y B φ) ↔ ∃*x(x A y(y B φ)))
4 df-rmo 2308 . . . . . 6 (∃*x A y B φ∃*x(x A y B φ))
5 19.42v 1783 . . . . . . 7 (y(x A (y B φ)) ↔ (x A y(y B φ)))
65mobii 1934 . . . . . 6 (∃*xy(x A (y B φ)) ↔ ∃*x(x A y(y B φ)))
73, 4, 63bitr4i 201 . . . . 5 (∃*x A y B φ∃*xy(x A (y B φ)))
8 2moex 1983 . . . . 5 (∃*xy(x A (y B φ)) → y∃*x(x A (y B φ)))
97, 8sylbi 114 . . . 4 (∃*x A y B φy∃*x(x A (y B φ)))
10 an12 495 . . . . . 6 ((x A (y B φ)) ↔ (y B (x A φ)))
1110mobii 1934 . . . . 5 (∃*x(x A (y B φ)) ↔ ∃*x(y B (x A φ)))
1211albii 1356 . . . 4 (y∃*x(x A (y B φ)) ↔ y∃*x(y B (x A φ)))
139, 12sylib 127 . . 3 (∃*x A y B φy∃*x(y B (x A φ)))
14 moanimv 1972 . . . 4 (∃*x(y B (x A φ)) ↔ (y B∃*x(x A φ)))
1514albii 1356 . . 3 (y∃*x(y B (x A φ)) ↔ y(y B∃*x(x A φ)))
1613, 15sylib 127 . 2 (∃*x A y B φy(y B∃*x(x A φ)))
17 df-ral 2305 . . 3 (y B ∃*x A φy(y B∃*x A φ))
18 df-rmo 2308 . . . . 5 (∃*x A φ∃*x(x A φ))
1918imbi2i 215 . . . 4 ((y B∃*x A φ) ↔ (y B∃*x(x A φ)))
2019albii 1356 . . 3 (y(y B∃*x A φ) ↔ y(y B∃*x(x A φ)))
2117, 20bitri 173 . 2 (y B ∃*x A φy(y B∃*x(x A φ)))
2216, 21sylibr 137 1 (∃*x A y B φy B ∃*x A φ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wal 1240  wex 1378   wcel 1390  ∃*wmo 1898  wral 2300  wrex 2301  ∃*wrmo 2303
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-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-ral 2305  df-rex 2306  df-rmo 2308
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator